5 lines
No EOL
205 B
Text
5 lines
No EOL
205 B
Text
fun : [`a, `b] ((`a -> `b) -> (`a -> `b)) -> `a -> `b -> `b
|
|
fix0 (f : (`a -> `b) -> (`a -> `b)) =
|
|
(\(a : `a) ->
|
|
(\(b : `b) -> f (\(x : `a) -> b : `a -> `b) a : `b -> `b)
|
|
: `a -> `b -> `b) |