package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/ltac2_plugin/Ltac2_plugin/Tac2expr/index.html

Module Ltac2_plugin.Tac2expr

type mutable_flag = bool
type rec_flag = bool
type redef_flag = bool
type lid = Names.Id.t
type uid = Names.Id.t
type ltac_constant = Names.KerName.t
type ltac_alias = Names.KerName.t
type ltac_notation = Names.KerName.t
type ltac_constructor = Names.KerName.t
type ltac_projection = Names.KerName.t
type type_constant = Names.KerName.t
type tacref =
  1. | TacConstant of ltac_constant
  2. | TacAlias of ltac_alias
type 'a or_relid =
  1. | RelId of Libnames.qualid
  2. | AbsKn of 'a
Misc
type ml_tactic_name = {
  1. mltac_plugin : string;
  2. mltac_tactic : string;
}
type 'a or_tuple =
  1. | Tuple of int
  2. | Other of 'a
Type syntax
type raw_typexpr_r =
  1. | CTypVar of Names.Name.t
  2. | CTypArrow of raw_typexpr * raw_typexpr
  3. | CTypRef of type_constant or_tuple or_relid * raw_typexpr list
and raw_typexpr = raw_typexpr_r CAst.t
type raw_typedef =
  1. | CTydDef of raw_typexpr option
  2. | CTydAlg of (Attributes.vernac_flags * uid * raw_typexpr list) list
  3. | CTydRec of (lid * mutable_flag * raw_typexpr) list
  4. | CTydOpn
type 'a glb_typexpr =
  1. | GTypVar of 'a
  2. | GTypArrow of 'a glb_typexpr * 'a glb_typexpr
  3. | GTypRef of type_constant or_tuple * 'a glb_typexpr list
type glb_alg_type = {
  1. galg_constructors : (UserWarn.t option * uid * int glb_typexpr list) list;
    (*

    Constructors of the algebraic type

    *)
  2. galg_nconst : int;
    (*

    Number of constant constructors

    *)
  3. galg_nnonconst : int;
    (*

    Number of non-constant constructors

    *)
}
type glb_typedef =
  1. | GTydDef of int glb_typexpr option
  2. | GTydAlg of glb_alg_type
  3. | GTydRec of (lid * mutable_flag * int glb_typexpr) list
  4. | GTydOpn
type type_scheme = int * int glb_typexpr
type raw_quant_typedef = Names.lident list * raw_typedef
type glb_quant_typedef = int * glb_typedef
Term syntax
type atom =
  1. | AtmInt of int
  2. | AtmStr of string
type ctor_indx =
  1. | Closed of int
  2. | Open of ltac_constructor
type ctor_data_for_patterns = {
  1. ctyp : type_constant option;
  2. cnargs : int;
  3. cindx : ctor_indx;
}
type glb_pat =
  1. | GPatVar of Names.Name.t
  2. | GPatAtm of atom
  3. | GPatRef of ctor_data_for_patterns * glb_pat list
  4. | GPatOr of glb_pat list
  5. | GPatAs of glb_pat * Names.Id.t
module PartialPat : sig ... end
type case_info = type_constant or_tuple
type 'a open_match = {
  1. opn_match : 'a;
  2. opn_branch : (Names.Name.t * Names.Name.t array * 'a) Names.KNmap.t;
    (*

    Invariant: should not be empty

    *)
  3. opn_default : Names.Name.t * 'a;
}
type glb_tacexpr =
  1. | GTacAtm of atom
  2. | GTacVar of Names.Id.t
  3. | GTacRef of ltac_constant
  4. | GTacFun of Names.Name.t list * glb_tacexpr
  5. | GTacApp of glb_tacexpr * glb_tacexpr list
  6. | GTacLet of rec_flag * (Names.Name.t * glb_tacexpr) list * glb_tacexpr
  7. | GTacCst of case_info * int * glb_tacexpr list
  8. | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Names.Name.t array * glb_tacexpr) array
  9. | GTacPrj of type_constant * glb_tacexpr * int
  10. | GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
  11. | GTacOpn of ltac_constructor * glb_tacexpr list
  12. | GTacWth of glb_tacexpr open_match
  13. | GTacFullMatch of glb_tacexpr * (glb_pat * glb_tacexpr) list
  14. | GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
  15. | GTacPrm of ml_tactic_name
type raw_patexpr_r =
  1. | CPatVar of Names.Name.t
  2. | CPatAtm of atom
  3. | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
  4. | CPatRecord of (ltac_projection or_relid * raw_patexpr) list
  5. | CPatCnv of raw_patexpr * raw_typexpr
  6. | CPatOr of raw_patexpr list
  7. | CPatAs of raw_patexpr * Names.lident

Tactic expressions

and raw_patexpr = raw_patexpr_r CAst.t
type raw_tacexpr_r =
  1. | CTacAtm of atom
  2. | CTacRef of tacref or_relid
  3. | CTacCst of ltac_constructor or_tuple or_relid
  4. | CTacFun of raw_patexpr list * raw_tacexpr
  5. | CTacApp of raw_tacexpr * raw_tacexpr list
  6. | CTacSyn of (Names.lname * raw_tacexpr) list * Names.KerName.t
  7. | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
  8. | CTacCnv of raw_tacexpr * raw_typexpr
  9. | CTacSeq of raw_tacexpr * raw_tacexpr
  10. | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
  11. | CTacCse of raw_tacexpr * raw_taccase list
  12. | CTacRec of raw_tacexpr option * raw_recexpr
  13. | CTacPrj of raw_tacexpr * ltac_projection or_relid
  14. | CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
  15. | CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
  16. | CTacGlb of int * (Names.lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr
    (*

    CTacGlb is essentially an expanded typed notation. Arguments bound with Anonymous have no type constraint.

    *)
and raw_tacexpr = raw_tacexpr_r CAst.t
and raw_taccase = raw_patexpr * raw_tacexpr
and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
Parsing & Printing
type exp_level =
  1. | E5
  2. | E4
  3. | E3
  4. | E2
  5. | E1
  6. | E0
type sexpr =
  1. | SexprStr of string CAst.t
  2. | SexprInt of int CAst.t
  3. | SexprRec of Loc.t * Names.Id.t option CAst.t * sexpr list
Toplevel statements
type strexpr =
  1. | StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
    (*

    Term definition

    *)
  2. | StrTyp of rec_flag * (Libnames.qualid * redef_flag * raw_quant_typedef) list
    (*

    Type definition

    *)
  3. | StrPrm of Names.lident * raw_typexpr * ml_tactic_name
    (*

    External definition

    *)
  4. | StrMut of Libnames.qualid * Names.lident option * raw_tacexpr
    (*

    Redefinition of mutable globals

    *)
type frame =
  1. | FrLtac of ltac_constant
  2. | FrAnon of glb_tacexpr
  3. | FrPrim of ml_tactic_name
  4. | FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
type backtrace = frame list