Pieuvre

A proof assistant based on the Calculus of Inductive Constructions, inspired by Rocq and written in OCaml.

This is the second project of the PROFON (functional project) course at ENS, implementing a proof assistant based on the Calculus of Inductive Constructions (CIC) and mimicking Rocq.

Contains complex (induction, inversion) and automatic (auto, semiring, . . . ) tactics, implicit arguments. Implementation of a VSCode extension.

🔗 Source repository