# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils coq 8.11.2 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.07.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.07.1 Official release 4.07.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 A library manager for OCaml # opam file: opam-version: "2.0" maintainer: "Hugo.Herbelin@inria.fr" homepage: "https://github.com/coq-contribs/intuitionistic-nuprl" license: "GPL" build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-R" "%{lib}%/coq/user-contrib/IntuitionisticNuprl"] depends: [ "ocaml" "coq" {>= "8.6" & < "8.7~"} ] tags: [ "keyword: Nuprl" "keyword: computational type theory" "keyword: extensional type theory" "keyword: intuitionistic type theory" "keyword: Howe's computational equivalence relation" "keyword: Partial Equivalence Relation (PER) semantics" "keyword: consistency" "keyword: continuity" "keyword: bar induction" "category: Mathematics/Logic/Type theory" ] authors: [ "Vincent Rahli <vincent.rahli@gmail.com> [http://www.cs.cornell.edu/~rahli/]" "Abhishek Anand <abhishek.anand.iitg@gmail.com> [http://www.cs.cornell.edu/~aa755/]" "Mark Bickford <mark.concertina@gmail.com> [http://nuprl.org/]" ] bug-reports: "https://github.com/coq-contribs/intuitionistic-nuprl/issues" dev-repo: "git+https://github.com/coq-contribs/intuitionistic-nuprl.git" synopsis: "An Impredicative Model of Nuprl's Constructive Type Theory" description: """ http://www.nuprl.org/html/Nuprl2Coq/ This library formalizes Nuprl's Constructive Type Theory (CTT) as of 2015. CTT is an extensional type theory originally inspired by Martin-Lof's extensional type theory, and that has since then been extended with several new types such as: intersection types, union types, image types, partial types, set types, quotient types, partial equivalence relation (per) types, simulation and bisimulation types, an atom type, and the "Base" type. Our formalization includes a definition of Nuprl's computation system, a definition of Howe's computational equivalence relation and a proof that it is a congruence, an impredicative definition of Nuprl's type system using Allen's PER semantics (using Prop's impredicativity, we can formalize Nuprl's infinite hierarchy of universes), definitions of most (but not all) of Nuprl's inference rules and proofs that these rules are valid w.r.t. Allen's PER semantics, and a proof of Nuprl's consistency. In addition to the standard introduction and elimination rules for Nuprl's types, we have also proved several Brouwerian rules. Our computation system also contains: (1) free choice sequences that we used to prove Bar Induction rules; (2) named exceptions and a "fresh" operator to generate fresh names, that we used to prove a continuity rule. More information can be found here: http://www.nuprl.org/html/Nuprl2Coq/ Feel free to send questions to the authors or to nuprl@cs.cornell.edu""" flags: light-uninstall url { src: "https://github.com/coq-contribs/intuitionistic-nuprl/archive/v8.6.0.tar.gz" checksum: "md5=30ee492d77b04371c77c4266d0fe678e" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-intuitionistic-nuprl.8.6.0 coq.8.11.2
[NOTE] Package coq is already installed (current version is 8.11.2). The following dependencies couldn't be met: - coq-intuitionistic-nuprl -> coq < 8.7~ -> ocaml < 4.06.0 base of this switch (use `--unlock-base' to force) No solution found, exiting
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
opam remove -y coq; opam install -y --show-action --unlock-base coq-intuitionistic-nuprl.8.6.0
true
true
No files were installed.
true