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