package rocq-runtime

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

Module Firstorder_core_plugin.FormulaSource

Sourcetype flags = {
  1. reds : RedFlags.reds;
}
Sourceval (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 'a -> 'a -> 'b -> 'b -> int
Sourceval (==?) : ('a -> 'a -> 'b -> 'b -> int) -> ('c -> 'c -> int) -> 'a -> 'a -> 'b -> 'b -> 'c -> 'c -> int
Sourcetype ('a, 'b) sum =
  1. | Left of 'a
  2. | Right of 'b
Sourcetype counter = bool -> Constr.metavariable
Sourceval construct_nhyps : Environ.env -> Constr.pinductive -> int array
Sourcemodule Env : sig ... end
Sourcetype atom
Sourceval hole_atom : atom
Sourceval repr_atom : Env.t -> atom -> EConstr.t
Sourceval compare_atom : atom -> atom -> int
Sourcetype atoms = {
  1. positive : atom list;
  2. negative : atom list;
}
Sourcetype _ side =
  1. | Hyp : bool -> [ `Hyp ] side
  2. | Concl : [ `Goal ] side
Sourcetype right_pattern =
  1. | Rarrow
  2. | Rand
  3. | Ror
  4. | Rfalse
  5. | Rforall
  6. | Rexists of Constr.metavariable * EConstr.constr * bool
Sourcetype left_arrow_pattern =
  1. | LLatom
  2. | LLfalse of Constr.pinductive * EConstr.constr list
  3. | LLand of Constr.pinductive * EConstr.constr list
  4. | LLor of Constr.pinductive * EConstr.constr list
  5. | LLforall of EConstr.constr
  6. | LLexists of Constr.pinductive * EConstr.constr list
  7. | LLarrow of EConstr.constr * EConstr.constr * EConstr.constr
Sourcetype left_pattern =
  1. | Lfalse
  2. | Land of Constr.pinductive
  3. | Lor of Constr.pinductive
  4. | Lforall of Constr.metavariable * EConstr.constr * bool
  5. | Lexists of Constr.pinductive
  6. | LA of atom * left_arrow_pattern
Sourcetype _ identifier = private
  1. | GoalId : [ `Goal ] identifier
  2. | FormulaId : Names.GlobRef.t -> [ `Hyp ] identifier
Sourceval goal_id : [ `Goal ] identifier
Sourceval formula_id : Environ.env -> Names.GlobRef.t -> [ `Hyp ] identifier
Sourcetype _ pattern =
  1. | LeftPattern : left_pattern -> [ `Hyp ] pattern
  2. | RightPattern : right_pattern -> [ `Goal ] pattern
Sourcetype 'a t = private {
  1. id : 'a identifier;
  2. constr : atom;
  3. pat : 'a pattern;
  4. atoms : atoms;
}
Sourcetype any_formula =
  1. | AnyFormula : 'a t -> any_formula
Sourceval build_formula : flags:flags -> Env.t -> Environ.env -> Evd.evar_map -> 'a side -> 'a identifier -> EConstr.types -> counter -> Env.t * ('a t, atom) sum
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