13 lines
No EOL
295 B
Markdown
13 lines
No EOL
295 B
Markdown
## Recall: System F
|
||
```agda
|
||
ℕ : Set₁
|
||
ℕ = ∀ {A} → (A → A) → A → A
|
||
zero : ℕ
|
||
zero = λ f x → x
|
||
suc : ℕ → ℕ
|
||
suc = λ n f x → f (n f x)
|
||
fold : ∀ {A} → (A → A) → A → ℕ → A
|
||
fold = λ f x n → n f x
|
||
-- add : ℕ → ℕ → ℕ
|
||
-- add = λ n → fold suc n
|
||
``` |