#STELLA

stella is a proof assistant written in MoonBit, still a work in progress. Version 0.2.0 provides its kernel: a bidirectional type checker for Martin-Löf type theory based on normalisation by evaluation, with the unit type, , , identity types with , W types and a cumulative universe hierarchy.

#Installation

moon add Luna-Flow/stella@0.2.0

Version 0.2.0 derives Debug instead of Show for its kernel types. Use debug_inspect(x), @debug.to_string(x) or Repr(x) where you previously used Show formatting.

// moon.pkg
import {
  "Luna-Flow/stella/elab",
  "moonbitlang/core/list",
}

#Example

using @elab {type TermInf}

test {
  // (λx. x : 1 → 1) has type 1 → 1, and applied to ⋆ it computes ⋆
  let id_unit = TermInf::Ann(Lam(Inf(Bound(0))), Inf(Pi(Inf(UnitType), Inf(UnitType))))
  let ty = @elab.type_inf_0(@list.empty(), id_unit)
  debug_inspect(@elab.quote(0, ty), content="Inf(Pi(Inf(UnitType), Inf(UnitType)))")
  let v = @elab.eval_inf(App(id_unit, UnitElement), @list.empty())
  debug_inspect(@elab.quote(0, v), content="UnitElement")
}

#Packages

Package	Contents
Luna-Flow/stella/elab	Core syntax, values, evaluation, read-back, bidirectional type checking

#Features

#Requirements

MoonBit toolchain with moonc 0.10 or newer. No dependencies besides the MoonBit core library.

#Documentation

Online manual (English, Chinese, Japanese): https://lunaflow.cn/en/stella/
English source: doc/manual/index.md, with the API reference, the tutorial (from the identity function to path induction and W-type recursion) and the design notes (typing rules, normalisation by evaluation, known gaps).
Changes between versions: CHANGELOG.md.

#References

#Contributing and contact

Read the design notes before changing the kernel, and run moon check --target all and moon test before opening a pull request.

[Chinese] Luna Flow QQ group: 762311556
[English/Japanese/Chinese] Email: zhehao0827 at 163.com

#License

Apache-2.0. See LICENSE.

Site source Report issue Packages Build queue Skills Statistics