Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/replicate
/
.
/
tests
/
lean
/
structInst1.lean.expected.out
blob: 408bf2f8ace9341bfb4dce19260a4911936d50cb [
file
] [
edit
]
structInst1
.
lean
:
12
:
11
-
12
:
19
:
error
:
field
'toA'
has already been specified
f5
(
c
:
C
)
(
a
:
A
)
:
C
f6
(
c
:
C
)
(
a
:
A
)
:
A
