Module Coq.AST

type int_size =
  1. | U8
  2. | U16
  3. | U32
  4. | U64
  5. | U128
  6. | USize
type int_type = {
  1. size : int_size;
  2. signed : Base.bool;
}
type ty =
  1. | WildTy
  2. | Bool
  3. | Unit
  4. | TypeTy
  5. | Int of int_type
  6. | NameTy of Base.string
  7. | RecordTy of Base.string * (Base.string * ty) Base.list
  8. | Product of ty Base.list
  9. | Coproduct of ty Base.list
  10. | Arrow of ty * ty
  11. | ArrayTy of ty * Base.string
  12. | SliceTy of ty
  13. | AppTy of ty * ty Base.list
  14. | NatMod of Base.string * Base.int * Base.string
  15. | Forall of Base.string Base.list * Base.string Base.list * ty
  16. | Exists of Base.string Base.list * Base.string Base.list * ty
type literal =
  1. | Const_string of Base.string
  2. | Const_char of Base.int
  3. | Const_int of Base.string * int_type
  4. | Const_bool of Base.bool
type pat =
  1. | WildPat
  2. | UnitPat
  3. | Ident of Base.string
  4. | Lit of literal
  5. | RecordPat of Base.string * (Base.string * pat) Base.list
  6. | ConstructorPat of Base.string * pat Base.list
  7. | TuplePat of pat Base.list
  8. | AscriptionPat of pat * ty
  9. | DisjunctivePat of pat Base.list
type monad_type =
  1. | Option
  2. | Result of ty
  3. | Exception of ty
type term =
  1. | UnitTerm
  2. | Let of let_args
  3. | If of term * term * term
  4. | Match of term * (pat * term) Base.list
  5. | Const of literal
  6. | Literal of Base.string
  7. | AppFormat of Base.string Base.list * notation_elements Base.list
  8. | App of term * term Base.list
  9. | Var of Base.string
  10. | NameTerm of Base.string
  11. | RecordConstructor of Base.string * (Base.string * term) Base.list
  12. | RecordUpdate of Base.string * term * (Base.string * term) Base.list
  13. | Type of ty
  14. | Lambda of pat Base.list * term
  15. | Tuple of term Base.list
  16. | Array of term Base.list
  17. | TypedTerm of term * ty
and notation_elements =
  1. | Newline of Base.int
  2. | Typing of ty * Base.bool * Base.int
  3. | Variable of pat * Base.int
  4. | Value of term * Base.bool * Base.int
and let_args = {
  1. pattern : pat;
  2. mut : Base.bool;
  3. value : term;
  4. body : term;
  5. value_typ : ty;
  6. monad_typ : monad_type Base.option;
}
type inductive_case =
  1. | InductiveCase of Base.string * ty
  2. | BaseCase of Base.string
type argument =
  1. | Implicit of pat * ty
  2. | Explicit of pat * ty
  3. | Typeclass of Base.string Base.option * ty
type definition_type = Base.string * argument Base.list * term * ty
type record_field =
  1. | Named of Base.string * ty
  2. | Coercion of Base.string * ty
type instance_decl =
  1. | InlineDef of definition_type
  2. | LetDef of definition_type
type instance_decls =
  1. | InstanceDecls of instance_decl Base.list
  2. | TermDef of term
type decl =
  1. | MultipleDecls of decl Base.list
  2. | Unimplemented of Base.string
  3. | Comment of Base.string
  4. | Definition of definition_type
  5. | ProgramDefinition of definition_type
  6. | Equations of definition_type
  7. | EquationsQuestionmark of definition_type
  8. | Notation of Base.string * term * Base.string Base.option
  9. | Record of Base.string * argument Base.list * record_field Base.list
  10. | Inductive of Base.string * argument Base.list * inductive_case Base.list
  11. | Class of Base.string * argument Base.list * record_field Base.list
  12. | Instance of Base.string * argument Base.list * ty * ty Base.list * definition_type Base.list
  13. | ProgramInstance of Base.string * argument Base.list * ty * ty Base.list * instance_decls
  14. | Require of Base.string Base.option * Base.string Base.list * Base.string Base.option
  15. | ModuleType of Base.string * argument Base.list * record_field Base.list
  16. | Module of Base.string * Base.string * argument Base.list * record_field Base.list
  17. | Parameter of Base.string * ty
  18. | HintUnfold of Base.string * ty Base.option