Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
missingDeclName.lean
blob: c71f884c30b464e280c1fbff27ae4d3663cd2670 [
file
] [
edit
]
def
foo
{α
β
:
Type
}
(
xs
:
Array
(α
×
β))
(
H
:
true
=
xs
.
all fun
(
x
,
y
)
=>
true
)
:
Unit
:=
()