package coq-hott

  1. Overview
  2. Homepage
The Homotopy Type Theory library

Install

Dune Dependency

Authors

Maintainers

Sources

V8.14.tar.gz
sha512=55a08bc76c90eb177bc22739bb6c2d95709575fdbc92c84c751c5fac3df6e71c5579c6d044572beb7c6d7696f257d58f4dd987af53ace12f11b77f7f5cb5daca

Description

To use the HoTT library, the following flags must be passed to coqc: -noinit -indices-matter To use the HoTT library in a project, add the following to _CoqProject: -arg -noinit -arg -indices-matter

Tags

logpath:HoTT

Published: 20 Oct 2021

Dependencies (3)

  1. coq >= "8.14" & < "8.15~"
  2. ocamlfind build
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover