Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
fun.lean
blob: d265e0baa8832ce0fbcdc58810939c00826b4e48 [
file
] [
edit
]
open
Function
Bool
opaque f
:
Nat
→
Bool
:=
default
opaque g
:
Nat
→
Nat
:=
default
#check f ∘ g ∘ g
#check (id : Nat → Nat)
opaque h
:
Nat
→
Bool
→
Nat
:=
default
opaque f1
:
Nat
→
Nat
→
Bool
:=
default
opaque f2
:
Bool
→
Nat
:=
default