Top 1,000 Features Creators Resources Extensions Blog Explorer CSV Download
GitHub icon

dedukti

< >

dedukti is a programming language created in 2009.

#916on PLDB 15Years Old
Download source code:
git clone https://github.com/Deducteam/Dedukti

Implementation of the λΠ-calculus modulo rewriting


Example from the web:
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).

Language features

Feature Supported Token Example
MultiLine Comments (; ;)
(; A comment
;)
Comments
(; This is a comment ;)
Semantic Indentation X

View source

- Build the next great programming language · About · Acknowledgements · Part of the World Wide Scroll