dedukti is a programming language created in 2009.
| #915on PLDB | 17Years Old |
git clone https://github.com/Deducteam/DeduktiImplementation of the λΠ-calculus modulo rewriting
Nat: Type.
zero: Nat.
succ: Nat -> Nat.
def plus: Nat -> Nat -> Nat.
[ n ] plus zero n --> n
[ n ] plus n zero --> n
[ n, m ] plus (succ n) m --> succ (plus n m)
[ n, m ] plus n (succ m) --> succ (plus n m).| Feature | Supported | Example | Token |
|---|---|---|---|
| MultiLine Comments | ✓ | (; A comment ;) | (; ;) |
| Comments | ✓ | (; A comment ;) | |
| Semantic Indentation | X |