package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/coq-core.interp/Constrexpr/index.html

Module ConstrexprSource

Concrete syntax for terms
Sourcetype sort_name_expr =
  1. | CSProp
  2. | CProp
  3. | CSet
  4. | CType of Libnames.qualid
  5. | CRawType of Univ.Level.t
    (*

    Universes like "foo.1" have no qualid form

    *)

Universes

Sourcetype sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen
Sourcetype instance_expr = univ_level_expr list

Constraints don't have anonymous universes

Sourcetype cumul_univ_decl_expr = ((Names.lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
Sourcetype ident_decl = Names.lident * universe_decl_expr option
Sourcetype cumul_ident_decl = Names.lident * cumul_univ_decl_expr option
Sourcetype name_decl = Names.lname * universe_decl_expr option
Sourcetype notation_with_optional_scope =
  1. | LastLonelyNotation
  2. | NotationInScope of string
Sourcetype entry_level = int
Sourcetype entry_relative_level =
  1. | LevelLt of entry_level
  2. | LevelLe of entry_level
  3. | LevelSome
Sourcetype notation_entry =
  1. | InConstrEntry
  2. | InCustomEntry of string
Sourcetype notation_entry_level =
  1. | InConstrEntrySomeLevel
  2. | InCustomEntryLevel of string * entry_level
Sourcetype notation_key = string
Sourcetype 'a or_by_notation_r =
  1. | AN of 'a
  2. | ByNotation of string * string option
Sourcetype 'a or_by_notation = 'a or_by_notation_r CAst.t
Sourcetype explicitation =
  1. | ExplByName of Names.Id.t
  2. | ExplByPos of int
Sourcetype binder_kind =
  1. | Default of Glob_term.binding_kind
  2. | Generalized of Glob_term.binding_kind * bool
    (*

    (Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses

    *)
Sourcetype explicit_flag = bool

true = with "@"

Sourcetype prim_token =
  1. | Number of NumTok.Signed.t
  2. | String of string
Sourcetype cases_pattern_expr_r =
  1. | CPatAlias of cases_pattern_expr * Names.lname
  2. | CPatCstr of Libnames.qualid * cases_pattern_expr list option * cases_pattern_expr list
    (*

    CPatCstr (_, c, Some l1, l2) represents (@ c l1) l2

    *)
  3. | CPatAtom of Libnames.qualid option
  4. | CPatOr of cases_pattern_expr list
  5. | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution * cases_pattern_expr list
    (*

    CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2

    *)
  6. | CPatPrim of prim_token
  7. | CPatRecord of (Libnames.qualid * cases_pattern_expr) list
  8. | CPatDelimiters of string * cases_pattern_expr
  9. | CPatCast of cases_pattern_expr * constr_expr

constr_expr is the abstract syntax tree produced by the parser

Sourceand cases_pattern_expr = cases_pattern_expr_r CAst.t
Sourceand kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
Sourceand cases_pattern_notation_substitution = cases_pattern_expr list * cases_pattern_expr list list
Sourceand constr_expr_r =
  1. | CRef of Libnames.qualid * instance_expr option
  2. | CFix of Names.lident * fix_expr list
  3. | CCoFix of Names.lident * cofix_expr list
  4. | CProdN of local_binder_expr list * constr_expr
  5. | CLambdaN of local_binder_expr list * constr_expr
  6. | CLetIn of Names.lname * constr_expr * constr_expr option * constr_expr
  7. | CAppExpl of Libnames.qualid * instance_expr option * constr_expr list
  8. | CApp of constr_expr * (constr_expr * explicitation CAst.t option) list
  9. | CProj of explicit_flag * Libnames.qualid * instance_expr option * (constr_expr * explicitation CAst.t option) list * constr_expr
  10. | CRecord of (Libnames.qualid * constr_expr) list
  11. | CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
  12. | CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
  13. | CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
  14. | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
  15. | CPatVar of Pattern.patvar
  16. | CEvar of Glob_term.existential_name CAst.t * (Names.lident * constr_expr) list
  17. | CSort of sort_expr
  18. | CCast of constr_expr * Constr.cast_kind * constr_expr
  19. | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
  20. | CGeneralization of Glob_term.binding_kind * constr_expr
  21. | CPrim of prim_token
  22. | CDelimiters of string * constr_expr
  23. | CArray of instance_expr option * constr_expr array * constr_expr * constr_expr
Sourceand constr_expr = constr_expr_r CAst.t
Sourceand case_expr = constr_expr * Names.lname option * cases_pattern_expr option
Sourceand branch_expr = (cases_pattern_expr list list * constr_expr) CAst.t
Sourceand recursion_order_expr_r =
  1. | CStructRec of Names.lident
  2. | CWfRec of Names.lident * constr_expr
  3. | CMeasureRec of Names.lident option * constr_expr * constr_expr option
    (*

    argument, measure, relation

    *)
Sourceand recursion_order_expr = recursion_order_expr_r CAst.t
Sourceand local_binder_expr =
  1. | CLocalAssum of Names.lname list * binder_kind * constr_expr
  2. | CLocalDef of Names.lname * constr_expr * constr_expr option
  3. | CLocalPattern of cases_pattern_expr
Sourceand constr_notation_substitution = constr_expr list * constr_expr list list * kinded_cases_pattern_expr list * local_binder_expr list list
Sourcetype constr_pattern_expr = constr_expr

Concrete syntax for modules and module types

Sourcetype with_declaration_ast =
  1. | CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
  2. | CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr
Sourcetype module_ast_r =
  1. | CMident of Libnames.qualid
  2. | CMapply of module_ast * module_ast
  3. | CMwith of module_ast * with_declaration_ast
Sourceand module_ast = module_ast_r CAst.t