Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/floatbits
/
.
/
tests
/
lean
/
autoImplicitChain.lean.expected.out
blob: b4d2707172aa2ea5fbe900d7767778f94933e54c [
file
] [
edit
]
def
f
:
{
a
:
A
}
→
{
a_1
:
B a
}
→
{
c
:
@C
a a_1
}
→
@D
a a_1 c
→
Bool
:=
fun
{
a
}
{
a_1
}
{
c
}
d
=>
true
