8 lines
166 B
Text
8 lines
166 B
Text
Set: pp::colors
|
||
Set: pp::unicode
|
||
Imported 'Int'
|
||
λ (A : Type) (a : A), let b := a in b : Π (A : Type), A → A
|
||
Assumed: g
|
||
Defined: f
|
||
f ℕ 10
|
||
f ℤ (- 10)
|