dedukti is a programming language created in 2009.
#900on PLDB | 15Years Old |
git clone https://github.com/Deducteam/Dedukti
Implementation 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 |