package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42
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