package rocq-runtime

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
OCaml

Innovation. Community. Security.