dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity
HITs-Examples/_CoqProject

7 lines
91 B
Plaintext
Raw Permalink Normal View History

Add a _CoqProject and a makefile
2017-05-01 19:25:27 +02:00
-R . "" COQC = hoqc COQDEP = hoqdep
Add a general hit recursion tactic. The tactic resolves the induction principle for a HIT using Canonical Structures, following the suggestion of @gallais
2017-05-18 17:43:19 +02:00
HitTactics.v
Add a _CoqProject and a makefile
2017-05-01 19:25:27 +02:00
Mod2.v
FinSets.v
Expressions.v
Integers.v