package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Elimination tactics.
type 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.

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

Implements user-level "destruct" and "induction"

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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