Kind-Core
Kind is a very raw and minimal Type Theory.
Usage
-
Clone and install this project
-
Use the
kindcommand to check/run terms
Grammar:
<Name> ::=
<alphanumeric-string>
<Numb> ::=
<json-number-literal>
<Term> ::=
| ALL: "∀(" <Name> ":" <Term> ")" <Term>
| LAM: "λ" <Name> <Term>
| APP: "(" <Term> <Term> ")"
| ANN: "{" <Name> ":" <Term> "}"
| SLF: "$(" <Name> ":" <Term> ")" <Term>
| INS: "~" <Term>
| DAT: "#[" <Term>* "]" "{" (<Ctor>)* "}"
| CON: "#" <Name> "{" <Term>* "}"
| SWI: "λ{0:" <Term> "_:" <Term> "}"
| MAT: "λ{" ("#" <Name> ":" <Term>)* "}"
| REF: <Name>
| LET: "let" <Name> "=" <Term> <Term>
| SET: "*"
| NUM: <Numb>
| OP2: "(" <Oper> <Term> <Term> ")"
| TXT: '"' <string-literal> '"'
| HOL: "?" <Name> ("[" <Term> ("," <Term>)* "]")?
| MET: "_" <Numb>
<Ctor> ::=
| "#" <Name> <Tele>
<Tele> ::=
| "{" (<Name> ":" <Term>)* "}" ":" <Term>
<Oper> ::=
| "+" | "-" | "*" | "/"
| "%" | "<=" | ">=" | "<"
| ">" | "==" | "!=" | "&"
| "|" | "^" | "<<" | ">>"