package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Compilation of pattern-matching
type pattern_matching_error =
  1. | BadPattern of Names.constructor * EConstr.constr
  2. | BadConstructor of Names.constructor * Names.inductive
  3. | WrongNumargConstructor of {
    1. cstr : Names.constructor;
    2. expanded : bool;
    3. nargs : int;
    4. expected_nassums : int;
    5. expected_ndecls : int;
    }
  4. | WrongNumargInductive of {
    1. ind : Names.inductive;
    2. expanded : bool;
    3. nargs : int;
    4. expected_nassums : int;
    5. expected_ndecls : int;
    }
  5. | UnusedClause of Glob_term.cases_pattern list
  6. | NonExhaustive of Glob_term.cases_pattern list
  7. | CannotInferPredicate of (EConstr.constr * EConstr.types) array

Pattern-matching errors

exception PatternMatchingError of Environ.env * Evd.evar_map * pattern_matching_error
val error_wrong_numarg_constructor : ?loc:Loc.t -> Environ.env -> cstr:Names.constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
val error_wrong_numarg_inductive : ?loc:Loc.t -> Environ.env -> ind:Names.inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
val irrefutable : Environ.env -> Glob_term.cases_pattern -> bool
Compilation primitive.
type 'a rhs = {
  1. rhs_env : GlobEnv.t;
  2. rhs_vars : Names.Id.Set.t;
  3. avoid_ids : Names.Id.Set.t;
  4. it : 'a option;
}
type 'a equation = {
  1. patterns : Glob_term.cases_pattern list;
  2. rhs : 'a rhs;
  3. alias_stack : Names.Name.t list;
  4. eqn_loc : Loc.t option;
  5. orig : int option;
  6. catch_all_vars : Names.Id.t CAst.t list;
}
type 'a matrix = 'a equation list
type tomatch_type =
  1. | IsInd of EConstr.types * Inductiveops.inductive_type * Names.Name.t list
  2. | NotInd of EConstr.constr option * EConstr.types
type tomatch_status =
  1. | Pushed of bool * ((EConstr.constr * tomatch_type) * int list * Names.Name.t)
  2. | Alias of bool * (Names.Name.t * EConstr.constr * (EConstr.constr * EConstr.types))
  3. | NonDepAlias
  4. | Abstract of int * EConstr.rel_declaration
type tomatch_stack = tomatch_status list
type pattern_history =
  1. | Top
  2. | MakeConstructor of Names.constructor * pattern_continuation
and pattern_continuation =
  1. | Continuation of int * Glob_term.cases_pattern list * pattern_history
  2. | Result of Glob_term.cases_pattern list
type 'a pattern_matching_problem = {
  1. env : GlobEnv.t;
  2. pred : EConstr.constr;
  3. tomatch : tomatch_stack;
  4. history : pattern_continuation;
  5. mat : 'a matrix;
  6. caseloc : Loc.t option;
  7. casestyle : Constr.case_style;
  8. typing_function : Evardefine.type_constraint -> GlobEnv.t -> Evd.evar_map -> 'a option -> Evd.evar_map * EConstr.unsafe_judgment;
}
val compile : program_mode:bool -> Evd.evar_map -> 'a pattern_matching_problem -> (int option * Names.Id.t CAst.t list) list * Evd.evar_map * EConstr.unsafe_judgment
val make_return_predicate_ltac_lvar : GlobEnv.t -> Evd.evar_map -> Names.Name.t -> Glob_term.glob_constr -> EConstr.constr -> GlobEnv.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