package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

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
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