package coq-hott

  1. Overview
  2. Homepage
The Homotopy Type Theory library

Install

Dune Dependency

Authors

Maintainers

Sources

V8.15.tar.gz
sha512=b1a656f6dc9c620cd83e798b8719ef013a8dbb955b30fd14e87aa5f8826ba76707d4abdb40ae341182859cb266d52c6be15725c7c501de5e52f398884ad7c590

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: 22 Jan 2022

Dependencies (3)

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

Dev Dependencies

None

Conflicts

None

Rocq

Interactive Theorem Prover