package coq-hott

  1. Overview
  2. Homepage
The Homotopy Type Theory library

Install

Dune Dependency

Authors

Maintainers

Sources

V8.16.tar.gz
sha512=7190e416abca853b4d84a57f9dc97b158bc80fb1b85f14a8fde0549401768b7b31ac04569f64ce003d69eedf3ae8f2ae9920584e0aaee11f9512a1482de0fe0e

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: 07 Sep 2022

Dependencies (3)

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

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover