package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.kernel/Primred/module-type-RedNativeEntries/index.html

Module type Primred.RedNativeEntriesSource

Sourcetype elem
Sourcetype args
Sourcetype evd
Sourcetype uinstance
Sourceval get : args -> int -> elem
Sourceval get_int : evd -> elem -> Uint63.t
Sourceval get_float : evd -> elem -> Float64.t
Sourceval get_string : evd -> elem -> Pstring.t
Sourceval get_parray : evd -> elem -> elem Parray.t
Sourceval mkInt : Environ.env -> Uint63.t -> elem
Sourceval mkFloat : Environ.env -> Float64.t -> elem
Sourceval mkString : Environ.env -> Pstring.t -> elem
Sourceval mkBool : Environ.env -> bool -> elem
Sourceval mkCarry : Environ.env -> bool -> elem -> elem
Sourceval mkIntPair : Environ.env -> elem -> elem -> elem
Sourceval mkFloatIntPair : Environ.env -> elem -> elem -> elem
Sourceval mkLt : Environ.env -> elem
Sourceval mkEq : Environ.env -> elem
Sourceval mkGt : Environ.env -> elem
Sourceval mkFLt : Environ.env -> elem
Sourceval mkFEq : Environ.env -> elem
Sourceval mkFGt : Environ.env -> elem
Sourceval mkFNotComparable : Environ.env -> elem
Sourceval mkPNormal : Environ.env -> elem
Sourceval mkNNormal : Environ.env -> elem
Sourceval mkPSubn : Environ.env -> elem
Sourceval mkNSubn : Environ.env -> elem
Sourceval mkPZero : Environ.env -> elem
Sourceval mkNZero : Environ.env -> elem
Sourceval mkPInf : Environ.env -> elem
Sourceval mkNInf : Environ.env -> elem
Sourceval mkNaN : Environ.env -> elem
Sourceval mkArray : Environ.env -> uinstance -> elem Parray.t -> elem -> elem