I am trying to understand what is possible with recursive types and what not. I read the docs and I think I do understand how to define a recursive type and how to manually construct instances:
let Nat = ∀(Nat_ : Type) → ∀(Zero_ : Nat_) → ∀(Succ_ : Nat_ → Nat_) → Nat_
let Zero
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) → Zero_
let One
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) → Succ_ Zero_
let Two
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) → Succ_ (Succ_ Zero_)
in Two
However what I do not know, is it possible to define a function
let Succ : Nat -> Nat = ...
such that e.g.
assert Two === Succ One
holds?
The real use case I am interested in is to define trees and graft trees together that might be defined in different files.