package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a or_var =
  1. | ArgArg of 'a
  2. | ArgVar of Names.lident
type !'a occurrences_gen =
  1. | AllOccurrences
  2. | AtLeastOneOccurrence
  3. | AllOccurrencesBut of 'a list
  4. | NoOccurrences
  5. | OnlyOccurrences of 'a list
type occurrences_expr = int or_var occurrences_gen
type !'a with_occurrences = occurrences_expr * 'a
type occurrences = int occurrences_gen
type hyp_location_flag =
  1. | InHyp
  2. | InHypTypeOnly
  3. | InHypValueOnly
type !'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
type !'id clause_expr = {
  1. onhyps : 'id hyp_location_expr list option;
  2. concl_occs : occurrences_expr;
}
type clause = Names.Id.t clause_expr
type clause_atom =
  1. | OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag
  2. | OnConcl of occurrences_expr
type concrete_clause = clause_atom list
type hyp_location = Names.Id.t * hyp_location_flag
type goal_location = hyp_location option
type simple_clause = Names.Id.t option list
type !'a or_like_first =
  1. | AtOccs of 'a
  2. | LikeFirst
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