package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
doc/coq-core.tactics/Induction/index.html
Module InductionSource
Elimination tactics.
Source
type elim_scheme = {elimt : EConstr.types;indref : Names.GlobRef.t option;params : EConstr.rel_context;(*(prm1,tprm1);(prm2,tprm2)...(prmp,tprmp)
*)nparams : int;(*number of parameters
*)predicates : EConstr.rel_context;(*(Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...)
*)npredicates : int;(*Number of predicates
*)branches : EConstr.rel_context;(*branchr,...,branch1
*)nbranches : int;(*Number of branches
*)args : EConstr.rel_context;(*(xni, Ti_ni) ... (x1, Ti_1)
*)nargs : int;(*number of arguments
*)indarg : EConstr.rel_declaration option;(*Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise
*)concl : EConstr.types;(*Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive
*)indarg_in_concl : bool;(*true if HI appears at the end of conclusion
*)farg_in_concl : bool;(*true if (f...) appears at the end of conclusion
*)
}rel_contexts and rel_declaration actually contain triples, and lists are actually in reverse order to fit compose_prod.
Source
val induction :
Tactics.evars_flag ->
Tactics.clear_flag ->
EConstr.constr ->
Tactypes.or_and_intro_pattern option ->
EConstr.constr Tactypes.with_bindings option ->
unit Proofview.tacticSource
val destruct :
Tactics.evars_flag ->
Tactics.clear_flag ->
EConstr.constr ->
Tactypes.or_and_intro_pattern option ->
EConstr.constr Tactypes.with_bindings option ->
unit Proofview.tacticGeneric case analysis / induction tactics.
Implements user-level "destruct" and "induction"
Source
val induction_destruct :
Tactics.rec_flag ->
Tactics.evars_flag ->
((Tactypes.delayed_open_constr_with_bindings Tactics.destruction_arg
* (Tactypes.intro_pattern_naming option
* Tactypes.or_and_intro_pattern option)
* Locus.clause option)
list
* EConstr.constr Tactypes.with_bindings option) ->
unit Proofview.tactic