Csepp 🌢Mar 20, 2022
#TIL about #lambdaPi and #dedukti , they seem nifty.
https://github.com/Deducteam/lambdapi
https://github.com/Deducteam/Dedukti
Looks like there are translators for the latter from languages like #Coq and #HOL .
cc #typeTheory
GitHub - Deducteam/lambdapi: Proof assistant based on the λΠ-calculus modulo rewriting

Proof assistant based on the λΠ-calculus modulo rewriting - GitHub - Deducteam/lambdapi: Proof assistant based on the λΠ-calculus modulo rewriting

GitHub