Skip to content

Latest commit

 

History

History
 
 

apps

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 

Applications written in Coq-Elpi

Derive

Given an inductive type declaration it synthesizes a bunch of useful stuff such as proved equality tests, projections, parametricity relations.

Eltac

A toy set of tactics implemented in Elpi.

NES

A Namespace Emulation System.