package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
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