mlang
mlang copied to clipboard
molikto
Towards changing things and see if it proofs
search `[issue 7]` in code for background, or see this commit 1855e9218c7388ce1b4bf1f19d6679fcaea2324c this issue only touch the parser and elaborator, don't touch the core
* color code name introduction, implicit name introduction and name usage, * color code keywords this will require when type checking, annotate Term.attributes, mutable field is fine!
the idea is `define with_constructors nat = ...` will define `suc` `zero` at the same level as `nat`. currently they are used as `nat.zero`