Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/Array.mapIdx
/
.
/
tests
/
lean
/
diamond3.lean
blob: 24bd9cee0ff8a8714388eccd896b6777fed63363 [
file
] [
edit
]
structure A
where
x
:
Nat
:=
0
y
:
Nat
:=
0
f
:
Nat
→
Nat
:=
(·
+
10
)
structure B
extends
A
where
z
:
Nat
structure C
extends
A
where
w
:
Nat
set_option structureDiamondWarning
false
structure D
extends
B
,
C
where
a
:
Nat
#print D.toC