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 . ∅
}