package coq-hott

  1. Overview
  2. Homepage
The Homotopy Type Theory library

Install

Dune Dependency

Authors

Maintainers

Sources

V8.18.tar.gz
sha512=e28cf6de90c0d99d6deb1fb8ffb14d57478c5894e8f3bfd1b21e6893cec22f33e4a5fb9d042035a83c88deb9d33e363394ef0788b616a4710ad94128ebfaa2ab

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 Aug 2023

Dependencies (4)

  1. coq >= "8.17.0" & < "8.19~"
  2. dune >= "3.5"
  3. ocamlfind build
  4. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover