* (2019-06-15 04:53:50 UTC)*

# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-num base Num library distributed with the OCaml compiler base-threads base base-unix base camlp5 7.06.10-g84ce6cc4 Preprocessor-pretty-printer of OCaml coq 8.5.3 Formal proof management system. num 0 The Num library for arbitrary-precision integer and rational arithmetic ocaml 4.05.0 The OCaml compiler (virtual package) ocaml-config 1 OCaml Switch Configuration ocaml-system 4.05.0 The OCaml compiler (system version, from outside of opam) # 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" }

- Command
`true`

- Return code
- 0

Dry install with the current Coq version:

- Command
`opam install -y --show-action coq-intuitionistic-nuprl.8.6.0 coq.8.5.3`

- Return code
- 5120
- Output
[NOTE] Package coq is already installed (current version is 8.5.3). The following dependencies couldn't be met: - coq-intuitionistic-nuprl -> coq >= 8.6 Your request can't be satisfied: - No available version of coq satisfies the constraints No solution found, exiting

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

- Command
`opam remove -y coq; opam install -y --show-action --unlock-base coq-intuitionistic-nuprl.8.6.0`

- Return code
- 0

- Command
`true`

- Return code
- 0
- Duration
- 0 s

- Command
`true`

- Return code
- 0
- Duration
- 0 s

No files were installed.

- Command
`true`

- Return code
- 0
- Missing removes
- none
- Wrong removes
- none