package universo

  1. Overview
  2. Docs
A tool for Dedukti to play with universes

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

  1. D
    dedukti-dev@inria.fr

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

v2.7.tar.gz
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/universo.common/Common/Logic/index.html

Module Common.LogicSource

Sourcemodule type LRA_REIFICATION = sig ... end
Sourcetype z =
  1. | Z
Sourcetype 'a s =
  1. | S
Sourcetype ('a, _) op =
  1. | True : 'a -> ('a, z) op
  2. | False : 'a -> ('a, z) op
  3. | Zero : 'a -> ('a, z) op
  4. | Succ : 'a -> ('a, z s) op
  5. | Minus : 'a -> ('a, z s) op
  6. | Eq : 'a -> ('a, z s s) op
  7. | Max : 'a -> ('a, z s s) op
  8. | IMax : 'a -> ('a, z s s) op
  9. | Le : 'a -> ('a, z s s) op
  10. | Ite : 'a -> ('a, z s s s) op
Sourcetype ('a, 'b) arrow =
  1. | Zero : 'b -> (z, 'b) arrow
  2. | One : ('b -> 'b) -> (z s, 'b) arrow
  3. | Two : ('b -> 'b -> 'b) -> (z s s, 'b) arrow
  4. | Three : ('b -> 'b -> 'b -> 'b) -> (z s s s, 'b) arrow
Sourcetype ('a, 'c) k = {
  1. mk : 'b. ('a, 'b) op -> ('b, 'c) arrow;
}
Sourcemodule type LRA_SPECIFICATION = sig ... end
Sourcetype theory = (Universes.pred * bool) list
Sourcemodule type QFUF_SPECIFICATION = sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct