to commemorate those fucking times
- It's trivial, just a toy, used to familiarize with Rust
- NO DEPENDENT TYPE
cargo run -- -i example/hello.ichigo
- core task
- parser
- type checker
- type inference
- evaluator
- peripheral task
- REPL
- pretty printer
- Algebraic data type
- Lambda calculus
- Pattern matching
- Unicode symbol
ℕ = σ {
0 : ℕ
1+ : ℕ → ℕ
}
+ = λ x : ℕ . λ {
1+ y . 1+ (+ x y)
0 . x
}
ℕ𝓁 = σ {
∅ : ℕ𝓁
++ : ℕ → ℕ𝓁 → ℕ𝓁
}
take = λ {
1+ n . λ {
∅ . ∅
++ x xs . ++ x (take n xs)
}
0 . λ x . ∅
}