package coq-hott

  1. Overview
  2. Homepage
The Homotopy Type Theory library

Install

Dune Dependency

Authors

Maintainers

Sources

V8.20.tar.gz
sha512=957e5f88a649235b7cbf0f3f089601183755fbf41fea3001c792945d8bc05ba1f6b22fa8765b0858d4fb1030b069c079e1764594ecfda482aa6975559e8f58b8

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: 28 Sep 2024

Dependencies (4)

  1. coq >= "8.19.0" & < "8.21~"
  2. dune >= "3.13"
  3. ocamlfind build
  4. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover