dan/HITs-Examples

mirror of https://github.com/nmvdw/HITs-Examples synced 2025-10-29 20:53:52 +01:00

Go to file

Niels van der Weide c6f756a856 Clarified proof of notIn_ext_union_singleton

2017-10-11 17:45:37 +02:00

Clarified proof of notIn_ext_union_singleton

2017-10-11 17:45:37 +02:00

Get a quotient from an implementation

2017-08-08 17:31:23 +02:00

_CoqProject

Add a general hit recursion tactic.

2017-05-18 17:43:19 +02:00

.gitignore

Better gitignore

2017-05-22 16:45:51 +02:00

Expressions.v

Expressions

2017-05-01 17:27:49 +02:00

Integers.v

Integers form a ring

2017-08-04 14:46:08 +02:00

Mod2.v

Replace the canonical structures mechanism for recursion with type classes

2017-05-22 21:06:13 +02:00

README.md

Improved README

2017-10-11 13:37:48 +02:00

README.md

HITs-Coq

Needed: https://github.com/HoTT/HoTT

The Finite Sets library of the 'Finite Sets in Homotopy Type Theory' is in the directory 'Finite Sets'.

The only part of the project that is buildable is the FiniteSets library.

Building

Before proceeding make sure that you have hoqc installed.

Build the HitTactics library in prelude.

cd prelude
hoqc HitTactics

Generate the Makefile and build the FiniteSets library

cd ../FiniteSets
coq_makefile -f _CoqProject -o Makefile
make