Skip to content

nmvdw/HITs-Examples

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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.

  1. Build the HitTactics library in prelude.
cd prelude
hoqc HitTactics
  1. Generate the Makefile and build the FiniteSets library
cd ../FiniteSets
coq_makefile -f _CoqProject -o Makefile
make

About

Examples of Higher Inductive Types

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors 4

  •  
  •  
  •  
  •  

Languages