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.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.tactics/Induction/index.html

Module InductionSource

Elimination tactics.
Sourcetype elim_scheme = {
  1. elimt : EConstr.types;
  2. indref : Names.GlobRef.t option;
  3. params : EConstr.rel_context;
    (*

    (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp)

    *)
  4. nparams : int;
    (*

    number of parameters

    *)
  5. predicates : EConstr.rel_context;
    (*

    (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...)

    *)
  6. npredicates : int;
    (*

    Number of predicates

    *)
  7. branches : EConstr.rel_context;
    (*

    branchr,...,branch1

    *)
  8. nbranches : int;
    (*

    Number of branches

    *)
  9. args : EConstr.rel_context;
    (*

    (xni, Ti_ni) ... (x1, Ti_1)

    *)
  10. nargs : int;
    (*

    number of arguments

    *)
  11. indarg : EConstr.rel_declaration option;
    (*

    Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise

    *)
  12. concl : EConstr.types;
    (*

    Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive

    *)
  13. indarg_in_concl : bool;
    (*

    true if HI appears at the end of conclusion

    *)
  14. 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.

Sourceval compute_elim_sig : Evd.evar_map -> EConstr.types -> elim_scheme
Generic case analysis / induction tactics.

Implements user-level "destruct" and "induction"