Reference
Auto-generated API reference from the MLTT type-checking kernel.

Verified

High-level combinators for writing kernel-checked implementations. Write programs with these combinators, then call v.verify to type-check and extract a Nix function that is correct by construction.

Example

# Verified successor: Nat → Nat
v.verify (H.forall "x" H.nat (_: H.nat))
         (v.fn "x" H.nat (x: H.succ x))
# → Nix function: n → n + 1

Literals

  • nat : Int → Hoas — natural number literal (S^n(zero))
  • str : String → Hoas — string literal
  • int_ : Int → Hoas — integer literal
  • float_ : Float → Hoas — float literal
  • true_, false_ — boolean literals
  • null_ — unit value (tt)

Binding

  • fn : String → Hoas → (Hoas → Hoas) → Hoas — lambda abstraction
  • let_ : String → Hoas → Hoas → (Hoas → Hoas) → Hoas — let binding

Data Operations

  • pair, fst, snd — Σ-type construction and projection
  • field : Hoas → String → Hoas → Hoas — record field projection by name
  • inl, inr — Sum injection
  • app — function application

Eliminators (Constant Motive)

These auto-generate the motive λ_.resultTy, so you only supply the result type and the branches:

  • if_ : Hoas → Hoas → { then_; else_; } → Hoas — Bool elimination
  • match : Hoas → Hoas → { zero; succ : k → ih → Hoas; } → Hoas — Nat elimination
  • matchList : Hoas → Hoas → Hoas → { nil; cons : h → t → ih → Hoas; } → Hoas — List elimination
  • matchSum : Hoas → Hoas → Hoas → Hoas → { left; right; } → Hoas — Sum elimination

Derived Combinators

  • map : Hoas → Hoas → Hoas → Hoas → Hoas — map f over a list
  • fold : Hoas → Hoas → Hoas → Hoas → Hoas → Hoas — fold over a list
  • filter : Hoas → Hoas → Hoas → Hoas — filter a list by predicate

Pipeline

  • verify : Hoas → Hoas → NixValue — type-check + eval + extract
←Value