Module `Constrexpr`Source

Concrete syntax for terms

Sourcetype sort_name_expr =

| CSProp
| CProp
| CSet
| CType of Libnames.qualid
| CRawType of Univ.Level.t
(*
Universes like "foo.1" have no qualid form
*)

Universes

Sourcetype univ_level_expr = sort_name_expr Glob_term.glob_sort_gen

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

Sourcetype instance_expr = univ_level_expr list

type univ_constraint_expr =
  sort_name_expr * Univ.constraint_type * sort_name_expr

Constraints don't have anonymous universes

Source

type universe_decl_expr =
  (Names.lident list, univ_constraint_expr list) UState.gen_universe_decl

Source

type 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 =

| LastLonelyNotation
| NotationInScope of string

Sourcetype entry_level = int

Sourcetype entry_relative_level =

| LevelLt of entry_level
| LevelLe of entry_level
| LevelSome

Sourcetype notation_entry =

| InConstrEntry
| InCustomEntry of string

Sourcetype notation_entry_level =

| InConstrEntrySomeLevel
| InCustomEntryLevel of string * entry_level

Sourcetype notation_key = string

Sourcetype notation = notation_entry * notation_key

Source

type specific_notation =
  notation_with_optional_scope * (notation_entry * notation_key)

Sourcetype 'a or_by_notation_r =

| AN of 'a
| ByNotation of string * string option

Sourcetype 'a or_by_notation = 'a or_by_notation_r CAst.t

Sourcetype explicitation =

| ExplByName of Names.Id.t
| ExplByPos of int

Sourcetype binder_kind =

| Default of Glob_term.binding_kind
| 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 =

| Number of NumTok.Signed.t
| String of string

Sourcetype cases_pattern_expr_r =

| CPatAlias of cases_pattern_expr * Names.lname
| CPatCstr of Libnames.qualid * cases_pattern_expr list option * cases_pattern_expr list
(*
CPatCstr (_, c, Some l1, l2) represents (@ c l1) l2
*)
| CPatAtom of Libnames.qualid option
| CPatOr of cases_pattern_expr list
| 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
*)
| CPatPrim of prim_token
| CPatRecord of (Libnames.qualid * cases_pattern_expr) list
| CPatDelimiters of string * cases_pattern_expr
| 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

Source

and cases_pattern_notation_substitution =
  cases_pattern_expr list * cases_pattern_expr list list

Sourceand constr_expr_r =

| CRef of Libnames.qualid * instance_expr option
| CFix of Names.lident * fix_expr list
| CCoFix of Names.lident * cofix_expr list
| CProdN of local_binder_expr list * constr_expr
| CLambdaN of local_binder_expr list * constr_expr
| CLetIn of Names.lname * constr_expr * constr_expr option * constr_expr
| CAppExpl of Libnames.qualid * instance_expr option * constr_expr list
| CApp of constr_expr * (constr_expr * explicitation CAst.t option) list
| CProj of explicit_flag * Libnames.qualid * instance_expr option * (constr_expr * explicitation CAst.t option) list * constr_expr
| CRecord of (Libnames.qualid * constr_expr) list
| CCases of Constr.case_style * constr_expr option * case_expr list * branch_expr list
| CLetTuple of Names.lname list * Names.lname option * constr_expr option * constr_expr * constr_expr
| CIf of constr_expr * Names.lname option * constr_expr option * constr_expr * constr_expr
| CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
| CPatVar of Pattern.patvar
| CEvar of Glob_term.existential_name CAst.t * (Names.lident * constr_expr) list
| CSort of sort_expr
| CCast of constr_expr * Constr.cast_kind * constr_expr
| CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
| 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

Source

and fix_expr =
  Names.lident
  * recursion_order_expr option
  * local_binder_expr list
  * constr_expr
  * constr_expr

Source

and cofix_expr =
  Names.lident * local_binder_expr list * constr_expr * constr_expr

Sourceand recursion_order_expr_r =

| CStructRec of Names.lident
| CWfRec of Names.lident * constr_expr
| 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 =

| CLocalAssum of Names.lname list * binder_kind * constr_expr
| CLocalDef of Names.lname * constr_expr * constr_expr option
| CLocalPattern of cases_pattern_expr

Source

and 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 =

| CWith_Module of Names.Id.t list CAst.t * Libnames.qualid
| CWith_Definition of Names.Id.t list CAst.t * universe_decl_expr option * constr_expr

Sourcetype module_ast_r =

| CMident of Libnames.qualid
| CMapply of module_ast * Libnames.qualid
| CMwith of module_ast * with_declaration_ast

Sourceand module_ast = module_ast_r CAst.t

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Constrexpr`Source

Concrete syntax for terms

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module ConstrexprSource

Concrete syntax for terms

Module `Constrexpr`Source