package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Proof format used by the proof-generating procedures. It is fairly close to Coq 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.

type prf_rule =
  1. | Annot of string * prf_rule
  2. | Hyp of int
  3. | Def of int
  4. | Ref of int
  5. | Cst of NumCompat.Q.t
  6. | Zero
  7. | Square of Vect.t
  8. | MulC of Vect.t * prf_rule
  9. | Gcd of 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
type 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
val pr_size : prf_rule -> NumCompat.Q.t
val pr_rule_max_def : prf_rule -> int
val pr_rule_max_hyp : prf_rule -> int
val proof_max_def : proof -> int
val normalise_proof : int -> proof -> int * proof
val output_prf_rule : out_channel -> prf_rule -> unit
val output_proof : out_channel -> proof -> unit
val add_proof : prf_rule -> prf_rule -> prf_rule
val mul_cst_proof : NumCompat.Q.t -> prf_rule -> prf_rule
val mul_proof : prf_rule -> prf_rule -> prf_rule
module Env : sig ... end
val compile_proof : Env.t -> proof -> Micromega.zArithProof
val cmpl_prf_rule : ('a Micromega.pExpr -> 'a Micromega.pol) -> (NumCompat.Q.t -> 'a) -> Env.t -> prf_rule -> 'a Micromega.psatz
val proof_of_farkas : prf_rule Mutils.IMap.t -> Vect.t -> prf_rule
val simplify_proof : proof -> proof * Mutils.ISet.t
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