package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

doc/coq-core.pretyping/Cases/index.html

Module CasesSource

Compilation of pattern-matching
Sourcetype 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

Sourceexception PatternMatchingError of Environ.env * Evd.evar_map * pattern_matching_error
Sourceval error_wrong_numarg_constructor : ?loc:Loc.t -> Environ.env -> cstr:Names.constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
Sourceval error_wrong_numarg_inductive : ?loc:Loc.t -> Environ.env -> ind:Names.inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
Sourceval irrefutable : Environ.env -> Glob_term.cases_pattern -> bool
Compilation primitive.
Sourcetype '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;
}
Sourcetype '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;
}
Sourcetype 'a matrix = 'a equation list
Sourcetype tomatch_type =
  1. | IsInd of EConstr.types * Inductiveops.inductive_type * Names.Name.t list
  2. | NotInd of EConstr.constr option * EConstr.types
Sourcetype 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
Sourcetype tomatch_stack = tomatch_status list
Sourcetype pattern_history =
  1. | Top
  2. | MakeConstructor of Names.constructor * pattern_continuation
Sourceand pattern_continuation =
  1. | Continuation of int * Glob_term.cases_pattern list * pattern_history
  2. | Result of Glob_term.cases_pattern list
Sourcetype '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;
}
Sourceval 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
Sourceval make_return_predicate_ltac_lvar : GlobEnv.t -> Evd.evar_map -> Names.Name.t -> Glob_term.glob_constr -> EConstr.constr -> GlobEnv.t