package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Polynomial.ProofFormatSource

Proof format used by the proof-generating procedures. It is fairly close to Rocq format but a bit more liberal.

It is used for proofs over Z, Q, R. However, certain constructions e.g. CutPrf are only relevant for Z.

Sourcetype prf_rule =
  1. | Annot of string * prf_rule
  2. | Hyp of int
  3. | Def of int
  4. | Ref of int
  5. | Cst of Micromega_core_plugin.NumCompat.Q.t
  6. | Zero
  7. | Square of Vect.t
  8. | MulC of Vect.t * prf_rule
  9. | Gcd of Micromega_core_plugin.NumCompat.Z.t * prf_rule
  10. | MulPrf of prf_rule * prf_rule
  11. | AddPrf of prf_rule * prf_rule
  12. | CutPrf of prf_rule
  13. | LetPrf of prf_rule * prf_rule
Sourcetype proof =
  1. | Done
  2. | Step of int * prf_rule * proof
  3. | Split of int * Vect.t * proof * proof
  4. | Enum of int * prf_rule * Vect.t * prf_rule * proof list
  5. | ExProof of int * int * int * var * var * var * proof
Sourceval normalise_proof : int -> proof -> int * proof
Sourceval output_prf_rule : Stdlib.out_channel -> prf_rule -> unit
Sourceval output_proof : Stdlib.out_channel -> proof -> unit
Sourceval add_proof : prf_rule -> prf_rule -> prf_rule
Sourceval mul_proof : prf_rule -> prf_rule -> prf_rule
Sourcemodule Env : 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