λProlog and the Calculus of Inductive Constructions

icon location Let's boost λProlog to implement an elaborator for CIC!

Results 2 repositories owned by λProlog and the Calculus of Inductive Constructions

elpi

262
Stars
32
Forks
Watchers

Embeddable Lambda Prolog Interpreter

verified publisher icon LPCIC

coq-elpi

128
Stars
48
Forks
Watchers

Coq plugin embedding elpi

verified publisher icon LPCIC