Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/Array.mapIdx
/
.
/
tests
/
lean
/
nonfatalattrs.lean.expected.out
blob: e30fbc8b60a6ec6153d0ba6b53b7795ed4cc9f22 [
file
] [
edit
]
nonfatalattrs
.
lean
:
6
:
2
-
6
:
19
:
error
:
unknown attribute
[
attrUnimplementedattr
]
foo
:
Nat
nonfatalattrs
.
lean
:
11
:
12
-
11
:
17
:
error
:
invalid
'class'
,
declaration
'bar.bar'
must be inductive datatype
,
structure
,
or
constant
bar
:
Nat
