molikto / mlang Goto Github PK

currently

define suc(a: nat) = nat.suc(a)

not accepted, but

define suc(a: nat): nat = nat.suc(a)

is

the idea is define with_constructors nat = ... will define suc zero at the same level as nat.

currently they are used as nat.zero

This can be simply done by adding the parameters in Inductively

search [issue 7] in code for background, or see this commit 1855e92

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!