hydra-0.15.0: src/main/haskell/Hydra/Coq/Syntax.hs

-- Note: this is an automatically generated file. Do not edit.

-- | A model for Coq core and extensions. Based on the Coq 8.15 grammar:
-- |   https://coq.github.io/doc/v8.15/refman/language/core/basic.html#essential-vocabulary
-- |   Extended with Vernacular commands for complete .v file generation.

module Hydra.Coq.Syntax where

import qualified Hydra.Core as Core
import Prelude hiding  (Enum, Ordering, decodeFloat, encodeFloat, fail, map, pure, sum)
import qualified Data.Scientific as Sci

data AnnotatedApplication =
  AnnotatedApplication {
    annotatedApplicationAnnot :: QualidAnnotated,
    annotatedApplicationTerms :: [Term1]}
  deriving (Eq, Ord, Read, Show)

_AnnotatedApplication = Core.Name "hydra.coq.syntax.AnnotatedApplication"

_AnnotatedApplication_annot = Core.Name "annot"

_AnnotatedApplication_terms = Core.Name "terms"

data Application =
  ApplicationNormal NormalApplication |
  ApplicationAnnotated AnnotatedApplication
  deriving (Eq, Ord, Read, Show)

_Application = Core.Name "hydra.coq.syntax.Application"

_Application_normal = Core.Name "normal"

_Application_annotated = Core.Name "annotated"

data Arg =
  ArgIdent IdentArg |
  ArgNatural NaturalArg |
  ArgTerm Term1
  deriving (Eq, Ord, Read, Show)

_Arg = Core.Name "hydra.coq.syntax.Arg"

_Arg_ident = Core.Name "ident"

_Arg_natural = Core.Name "natural"

_Arg_term = Core.Name "term"

data Binder =
  BinderName Name |
  BinderType TypeBinders |
  BinderTerm LetBinder |
  BinderImplicit ImplicitBinders |
  BinderGeneralizing GeneralizingBinder |
  BinderPattern Pattern0
  deriving (Eq, Ord, Read, Show)

_Binder = Core.Name "hydra.coq.syntax.Binder"

_Binder_name = Core.Name "name"

_Binder_type = Core.Name "type"

_Binder_term = Core.Name "term"

_Binder_implicit = Core.Name "implicit"

_Binder_generalizing = Core.Name "generalizing"

_Binder_pattern = Core.Name "pattern"

data CaseItem =
  CaseItem {
    caseItemTerm :: Term100,
    caseItemAs :: (Maybe Name),
    caseItemIn :: (Maybe Pattern)}
  deriving (Eq, Ord, Read, Show)

_CaseItem = Core.Name "hydra.coq.syntax.CaseItem"

_CaseItem_term = Core.Name "term"

_CaseItem_as = Core.Name "as"

_CaseItem_in = Core.Name "in"

data Cofix =
  Cofix {
    cofixBody :: CofixBody,
    cofixQual :: (Maybe CofixQual)}
  deriving (Eq, Ord, Read, Show)

_Cofix = Core.Name "hydra.coq.syntax.Cofix"

_Cofix_body = Core.Name "body"

_Cofix_qual = Core.Name "qual"

data CofixBody =
  CofixBody {
    cofixBodyIdent :: Ident,
    cofixBodyBinders :: [Binder],
    cofixBodyType :: (Maybe Type),
    cofixBodyTerm :: Term}
  deriving (Eq, Ord, Read, Show)

_CofixBody = Core.Name "hydra.coq.syntax.CofixBody"

_CofixBody_ident = Core.Name "ident"

_CofixBody_binders = Core.Name "binders"

_CofixBody_type = Core.Name "type"

_CofixBody_term = Core.Name "term"

data CofixQual =
  CofixQualIn Term |
  CofixQualWith CofixWith
  deriving (Eq, Ord, Read, Show)

_CofixQual = Core.Name "hydra.coq.syntax.CofixQual"

_CofixQual_in = Core.Name "in"

_CofixQual_with = Core.Name "with"

data CofixWith =
  CofixWith {
    cofixWithWith :: [CofixBody],
    cofixWithFor :: (Maybe Ident)}
  deriving (Eq, Ord, Read, Show)

_CofixWith = Core.Name "hydra.coq.syntax.CofixWith"

_CofixWith_with = Core.Name "with"

_CofixWith_for = Core.Name "for"

data Equation =
  Equation {
    equationPattern :: [[Pattern]],
    equationTerm :: Term}
  deriving (Eq, Ord, Read, Show)

_Equation = Core.Name "hydra.coq.syntax.Equation"

_Equation_pattern = Core.Name "pattern"

_Equation_term = Core.Name "term"

data ExistentialVariable =
  ExistentialVariable {
    existentialVariableIdent :: Ident,
    existentialVariableVariant :: ExistentialVariableVariant}
  deriving (Eq, Ord, Read, Show)

_ExistentialVariable = Core.Name "hydra.coq.syntax.ExistentialVariable"

_ExistentialVariable_ident = Core.Name "ident"

_ExistentialVariable_variant = Core.Name "variant"

data ExistentialVariableVariant =
  ExistentialVariableVariantPlaceholder  |
  ExistentialVariableVariantInside1  |
  ExistentialVariableVariantInside2  |
  ExistentialVariableVariantOutside (Maybe IdentArg)
  deriving (Eq, Ord, Read, Show)

_ExistentialVariableVariant = Core.Name "hydra.coq.syntax.ExistentialVariableVariant"

_ExistentialVariableVariant_placeholder = Core.Name "placeholder"

_ExistentialVariableVariant_inside1 = Core.Name "inside1"

_ExistentialVariableVariant_inside2 = Core.Name "inside2"

_ExistentialVariableVariant_outside = Core.Name "outside"

newtype FieldIdent =
  FieldIdent {
    unFieldIdent :: Ident}
  deriving (Eq, Ord, Read, Show)

_FieldIdent = Core.Name "hydra.coq.syntax.FieldIdent"

data Fix =
  FixDecl Fix_Decl |
  FixQual (Maybe Fix_Qual)
  deriving (Eq, Ord, Read, Show)

_Fix = Core.Name "hydra.coq.syntax.Fix"

_Fix_decl = Core.Name "decl"

_Fix_qual = Core.Name "qual"

data FixAnnot =
  FixAnnotStruct Ident |
  FixAnnotWf FixAnnot_Wf |
  FixAnnotMeasure FixAnnot_Measure
  deriving (Eq, Ord, Read, Show)

_FixAnnot = Core.Name "hydra.coq.syntax.FixAnnot"

_FixAnnot_struct = Core.Name "struct"

_FixAnnot_wf = Core.Name "wf"

_FixAnnot_measure = Core.Name "measure"

data FixAnnot_Measure =
  FixAnnot_Measure {
    fixAnnot_MeasureTerm :: OneTerm,
    fixAnnot_MeasureIdent :: (Maybe Ident),
    fixAnnot_MeasureTerm2 :: (Maybe OneTerm)}
  deriving (Eq, Ord, Read, Show)

_FixAnnot_Measure = Core.Name "hydra.coq.syntax.FixAnnot_Measure"

_FixAnnot_Measure_term = Core.Name "term"

_FixAnnot_Measure_ident = Core.Name "ident"

_FixAnnot_Measure_term2 = Core.Name "term2"

data FixAnnot_Wf =
  FixAnnot_Wf {
    fixAnnot_WfTerm :: OneTerm,
    fixAnnot_WfIdent :: Ident}
  deriving (Eq, Ord, Read, Show)

_FixAnnot_Wf = Core.Name "hydra.coq.syntax.FixAnnot_Wf"

_FixAnnot_Wf_term = Core.Name "term"

_FixAnnot_Wf_ident = Core.Name "ident"

data Fix_Decl =
  Fix_Decl {
    fix_DeclIdent :: Ident,
    fix_DeclBinders :: [Binder],
    fix_DeclAnnot :: (Maybe FixAnnot),
    fix_DeclType :: (Maybe Type),
    fix_DeclTerm :: Term}
  deriving (Eq, Ord, Read, Show)

_Fix_Decl = Core.Name "hydra.coq.syntax.Fix_Decl"

_Fix_Decl_ident = Core.Name "ident"

_Fix_Decl_binders = Core.Name "binders"

_Fix_Decl_annot = Core.Name "annot"

_Fix_Decl_type = Core.Name "type"

_Fix_Decl_term = Core.Name "term"

data Fix_Qual =
  Fix_QualIn Term |
  Fix_QualWith FixWith
  deriving (Eq, Ord, Read, Show)

_Fix_Qual = Core.Name "hydra.coq.syntax.Fix_Qual"

_Fix_Qual_in = Core.Name "in"

_Fix_Qual_with = Core.Name "with"

data FixWith =
  FixWith {
    fixWithDecls :: [Fix_Decl],
    fixWithFor :: (Maybe Ident)}
  deriving (Eq, Ord, Read, Show)

_FixWith = Core.Name "hydra.coq.syntax.FixWith"

_FixWith_decls = Core.Name "decls"

_FixWith_for = Core.Name "for"

data Forall =
  Forall {
    forallBinders :: OpenBinders,
    forallType :: Type}
  deriving (Eq, Ord, Read, Show)

_Forall = Core.Name "hydra.coq.syntax.Forall"

_Forall_binders = Core.Name "binders"

_Forall_type = Core.Name "type"

data ForallOrFun =
  ForallOrFunForall Forall |
  ForallOrFunFun Fun
  deriving (Eq, Ord, Read, Show)

_ForallOrFun = Core.Name "hydra.coq.syntax.ForallOrFun"

_ForallOrFun_forall = Core.Name "forall"

_ForallOrFun_fun = Core.Name "fun"

data Fun =
  Fun {
    funBinders :: OpenBinders,
    funBody :: Term}
  deriving (Eq, Ord, Read, Show)

_Fun = Core.Name "hydra.coq.syntax.Fun"

_Fun_binders = Core.Name "binders"

_Fun_body = Core.Name "body"

data GeneralizingBinder =
  -- | Terms surrounded by `( ) introduce their free variables as explicit arguments
  GeneralizingBinderExplicit TypeclassConstraint |
  -- | Terms surrounded by `{ } introduce their free variables as maximally inserted implicit arguments
  GeneralizingBinderImplicitMaximallyInserted TypeclassConstraint |
  -- | Terms surrounded by `[ ] introduce them as non-maximally inserted implicit arguments
  GeneralizingBinderImplicitNonMaximallyInserted TypeclassConstraint
  deriving (Eq, Ord, Read, Show)

_GeneralizingBinder = Core.Name "hydra.coq.syntax.GeneralizingBinder"

_GeneralizingBinder_explicit = Core.Name "explicit"

_GeneralizingBinder_implicitMaximallyInserted = Core.Name "implicitMaximallyInserted"

_GeneralizingBinder_implicitNonMaximallyInserted = Core.Name "implicitNonMaximallyInserted"

newtype Ident =
  Ident {
    unIdent :: String_}
  deriving (Eq, Ord, Read, Show)

_Ident = Core.Name "hydra.coq.syntax.Ident"

data IdentArg =
  IdentArg {
    identArgIdent :: Ident,
    identArgTerm :: Term}
  deriving (Eq, Ord, Read, Show)

_IdentArg = Core.Name "hydra.coq.syntax.IdentArg"

_IdentArg_ident = Core.Name "ident"

_IdentArg_term = Core.Name "term"

-- | Pattern match on boolean values
data If =
  If {
    ifCondition :: Term,
    ifReturnAs :: (Maybe ReturnAs),
    ifThen :: Term,
    ifElse :: Term}
  deriving (Eq, Ord, Read, Show)

_If = Core.Name "hydra.coq.syntax.If"

_If_condition = Core.Name "condition"

_If_returnAs = Core.Name "returnAs"

_If_then = Core.Name "then"

_If_else = Core.Name "else"

-- | In the context of a function definition, these forms specify that name is an implicit argument.
data ImplicitBinders =
  -- | The first form, with curly braces, makes name a maximally inserted implicit argument
  ImplicitBindersMaximallyInserted TypeBinders |
  -- | The second form, with square brackets, makes name a non-maximally inserted implicit argument.
  ImplicitBindersNonMaximallyInserted TypeBinders
  deriving (Eq, Ord, Read, Show)

_ImplicitBinders = Core.Name "hydra.coq.syntax.ImplicitBinders"

_ImplicitBinders_maximallyInserted = Core.Name "maximallyInserted"

_ImplicitBinders_nonMaximallyInserted = Core.Name "nonMaximallyInserted"

-- | A let-in definition
data Let =
  Let {
    letBindings :: LetBindings,
    letIn :: Term}
  deriving (Eq, Ord, Read, Show)

_Let = Core.Name "hydra.coq.syntax.Let"

_Let_bindings = Core.Name "bindings"

_Let_in = Core.Name "in"

-- | Some constructions allow the binding of a variable to value. This is called a 'let-binder'.
data LetBinder =
  LetBinder {
    letBinderName :: Name,
    letBinderType :: (Maybe Type),
    letBinderTerm :: Term}
  deriving (Eq, Ord, Read, Show)

_LetBinder = Core.Name "hydra.coq.syntax.LetBinder"

_LetBinder_name = Core.Name "name"

_LetBinder_type = Core.Name "type"

_LetBinder_term = Core.Name "term"

data LetBindings =
  LetBindingsNamed LetNamed |
  LetBindingsDestructuring LetDestructuring
  deriving (Eq, Ord, Read, Show)

_LetBindings = Core.Name "hydra.coq.syntax.LetBindings"

_LetBindings_named = Core.Name "named"

_LetBindings_destructuring = Core.Name "destructuring"

data LetNamed =
  LetNamed {
    letNamedBinder :: LetBinder,
    letNamedBinders :: [Binder]}
  deriving (Eq, Ord, Read, Show)

_LetNamed = Core.Name "hydra.coq.syntax.LetNamed"

_LetNamed_binder = Core.Name "binder"

_LetNamed_binders = Core.Name "binders"

data LetDestructuring =
  LetDestructuringVariant1 LetDestructuring_Variant1 |
  LetDestructuringVariant2 LetDestructuring_Variant2 |
  LetDestructuringVariant3 LetDestructuring_Variant3
  deriving (Eq, Ord, Read, Show)

_LetDestructuring = Core.Name "hydra.coq.syntax.LetDestructuring"

_LetDestructuring_variant1 = Core.Name "variant1"

_LetDestructuring_variant2 = Core.Name "variant2"

_LetDestructuring_variant3 = Core.Name "variant3"

data LetDestructuring_Variant1 =
  LetDestructuring_Variant1 {
    letDestructuring_Variant1Names :: [Name],
    letDestructuring_Variant1ReturnAs :: (Maybe ReturnAs),
    letDestructuring_Variant1Term :: Term}
  deriving (Eq, Ord, Read, Show)

_LetDestructuring_Variant1 = Core.Name "hydra.coq.syntax.LetDestructuring_Variant1"

_LetDestructuring_Variant1_names = Core.Name "names"

_LetDestructuring_Variant1_returnAs = Core.Name "returnAs"

_LetDestructuring_Variant1_term = Core.Name "term"

data LetDestructuring_Variant2 =
  LetDestructuring_Variant2 {
    letDestructuring_Variant2Pattern :: Pattern,
    letDestructuring_Variant2Term :: Term,
    letDestructuring_Variant2Return :: (Maybe Term100)}
  deriving (Eq, Ord, Read, Show)

_LetDestructuring_Variant2 = Core.Name "hydra.coq.syntax.LetDestructuring_Variant2"

_LetDestructuring_Variant2_pattern = Core.Name "pattern"

_LetDestructuring_Variant2_term = Core.Name "term"

_LetDestructuring_Variant2_return = Core.Name "return"

data LetDestructuring_Variant3 =
  LetDestructuring_Variant3 {
    letDestructuring_Variant3Pattern1 :: Pattern,
    letDestructuring_Variant3Pattern2 :: Pattern,
    letDestructuring_Variant3Term :: Term,
    letDestructuring_Variant3Return :: Term100}
  deriving (Eq, Ord, Read, Show)

_LetDestructuring_Variant3 = Core.Name "hydra.coq.syntax.LetDestructuring_Variant3"

_LetDestructuring_Variant3_pattern1 = Core.Name "pattern1"

_LetDestructuring_Variant3_pattern2 = Core.Name "pattern2"

_LetDestructuring_Variant3_term = Core.Name "term"

_LetDestructuring_Variant3_return = Core.Name "return"

data Match =
  Match {
    matchCaseItems :: [CaseItem],
    matchReturn :: (Maybe Term100),
    matchPipe :: Bool,
    matchEquations :: [Equation]}
  deriving (Eq, Ord, Read, Show)

_Match = Core.Name "hydra.coq.syntax.Match"

_Match_caseItems = Core.Name "caseItems"

_Match_return = Core.Name "return"

_Match_pipe = Core.Name "pipe"

_Match_equations = Core.Name "equations"

newtype Name =
  Name {
    unName :: (Maybe Ident)}
  deriving (Eq, Ord, Read, Show)

_Name = Core.Name "hydra.coq.syntax.Name"

-- | A non-negative arbitrary-precision integer
newtype Natural =
  Natural {
    unNatural :: Integer}
  deriving (Eq, Ord, Read, Show)

_Natural = Core.Name "hydra.coq.syntax.Natural"

data NaturalArg =
  NaturalArg {
    naturalArgNatural :: Natural,
    naturalArgTerm :: Term}
  deriving (Eq, Ord, Read, Show)

_NaturalArg = Core.Name "hydra.coq.syntax.NaturalArg"

_NaturalArg_natural = Core.Name "natural"

_NaturalArg_term = Core.Name "term"

data NormalApplication =
  NormalApplication {
    normalApplicationLhs :: Term1,
    normalApplicationRhs :: [Arg]}
  deriving (Eq, Ord, Read, Show)

_NormalApplication = Core.Name "hydra.coq.syntax.NormalApplication"

_NormalApplication_lhs = Core.Name "lhs"

_NormalApplication_rhs = Core.Name "rhs"

newtype Number =
  Number {
    unNumber :: Double}
  deriving (Eq, Ord, Read, Show)

_Number = Core.Name "hydra.coq.syntax.Number"

data OneTerm =
  OneTermExplicit QualidAnnotated |
  OneTermTerm1 Term1
  deriving (Eq, Ord, Read, Show)

_OneTerm = Core.Name "hydra.coq.syntax.OneTerm"

_OneTerm_explicit = Core.Name "explicit"

_OneTerm_term1 = Core.Name "term1"

data OpenBinders =
  OpenBindersType TypeBinders |
  OpenBindersBinders [Binder]
  deriving (Eq, Ord, Read, Show)

_OpenBinders = Core.Name "hydra.coq.syntax.OpenBinders"

_OpenBinders_type = Core.Name "type"

_OpenBinders_binders = Core.Name "binders"

data Pattern =
  PatternPattern Pattern10 |
  PatternTerm (Maybe Term)
  deriving (Eq, Ord, Read, Show)

_Pattern = Core.Name "hydra.coq.syntax.Pattern"

_Pattern_pattern = Core.Name "pattern"

_Pattern_term = Core.Name "term"

data Pattern0 =
  Pattern0Qualid Qualid |
  Pattern0QualIdAndPattern QualidAndPattern |
  Pattern0Placeholder  |
  Pattern0Parens [Pattern] |
  Pattern0Number Number |
  Pattern0String String_
  deriving (Eq, Ord, Read, Show)

_Pattern0 = Core.Name "hydra.coq.syntax.Pattern0"

_Pattern0_qualid = Core.Name "qualid"

_Pattern0_qualIdAndPattern = Core.Name "qualIdAndPattern"

_Pattern0_placeholder = Core.Name "placeholder"

_Pattern0_parens = Core.Name "parens"

_Pattern0_number = Core.Name "number"

_Pattern0_string = Core.Name "string"

data Pattern1 =
  Pattern1 {
    pattern1Pattern :: Pattern0,
    pattern1Scope :: (Maybe ScopeKey)}
  deriving (Eq, Ord, Read, Show)

_Pattern1 = Core.Name "hydra.coq.syntax.Pattern1"

_Pattern1_pattern = Core.Name "pattern"

_Pattern1_scope = Core.Name "scope"

data Pattern10 =
  Pattern10As Pattern10_As |
  Pattern10Patterns Pattern10_Patterns |
  Pattern10Qualiid Pattern10_Qualid
  deriving (Eq, Ord, Read, Show)

_Pattern10 = Core.Name "hydra.coq.syntax.Pattern10"

_Pattern10_as = Core.Name "as"

_Pattern10_patterns = Core.Name "patterns"

_Pattern10_qualiid = Core.Name "qualiid"

data Pattern10_As =
  Pattern10_As {
    pattern10_AsPattern :: Pattern1,
    pattern10_AsAs :: Name}
  deriving (Eq, Ord, Read, Show)

_Pattern10_As = Core.Name "hydra.coq.syntax.Pattern10_As"

_Pattern10_As_pattern = Core.Name "pattern"

_Pattern10_As_as = Core.Name "as"

data Pattern10_Patterns =
  Pattern10_Patterns {
    pattern10_PatternsPattern :: Pattern1,
    pattern10_PatternsPatterns :: [Pattern1]}
  deriving (Eq, Ord, Read, Show)

_Pattern10_Patterns = Core.Name "hydra.coq.syntax.Pattern10_Patterns"

_Pattern10_Patterns_pattern = Core.Name "pattern"

_Pattern10_Patterns_patterns = Core.Name "patterns"

data Pattern10_Qualid =
  Pattern10_Qualid {
    pattern10_QualidQualid :: Qualid,
    pattern10_QualidPatterns :: [Pattern1]}
  deriving (Eq, Ord, Read, Show)

_Pattern10_Qualid = Core.Name "hydra.coq.syntax.Pattern10_Qualid"

_Pattern10_Qualid_qualid = Core.Name "qualid"

_Pattern10_Qualid_patterns = Core.Name "patterns"

data PrimitiveNotations =
  PrimitiveNotationsNumber Number |
  PrimitiveNotationsString String_
  deriving (Eq, Ord, Read, Show)

_PrimitiveNotations = Core.Name "hydra.coq.syntax.PrimitiveNotations"

_PrimitiveNotations_number = Core.Name "number"

_PrimitiveNotations_string = Core.Name "string"

-- | A qualified identifier
data Qualid =
  Qualid {
    qualidId :: Ident,
    qualidFieldIds :: [FieldIdent]}
  deriving (Eq, Ord, Read, Show)

_Qualid = Core.Name "hydra.coq.syntax.Qualid"

_Qualid_id = Core.Name "id"

_Qualid_fieldIds = Core.Name "fieldIds"

data QualidAndPattern =
  QualidAndPattern {
    qualidAndPatternQualid :: Qualid,
    qualidAndPatternPattern :: Pattern}
  deriving (Eq, Ord, Read, Show)

_QualidAndPattern = Core.Name "hydra.coq.syntax.QualidAndPattern"

_QualidAndPattern_qualid = Core.Name "qualid"

_QualidAndPattern_pattern = Core.Name "pattern"

data QualidAnnotated =
  QualidAnnotated {
    qualidAnnotatedQualid :: Qualid,
    qualidAnnotatedUnivAnnot :: (Maybe UnivAnnot)}
  deriving (Eq, Ord, Read, Show)

_QualidAnnotated = Core.Name "hydra.coq.syntax.QualidAnnotated"

_QualidAnnotated_qualid = Core.Name "qualid"

_QualidAnnotated_univAnnot = Core.Name "univAnnot"

data ReturnAs =
  ReturnAs {
    returnAsAs :: (Maybe Name),
    returnAsReturn :: Term100}
  deriving (Eq, Ord, Read, Show)

_ReturnAs = Core.Name "hydra.coq.syntax.ReturnAs"

_ReturnAs_as = Core.Name "as"

_ReturnAs_return = Core.Name "return"

newtype ScopeKey =
  ScopeKey {
    unScopeKey :: Ident}
  deriving (Eq, Ord, Read, Show)

_ScopeKey = Core.Name "hydra.coq.syntax.ScopeKey"

-- | The types of types are called sorts.
data Sort =
  -- | The sort 𝖲𝖾𝗍 intends to be the type of small sets.
  SortSet  |
  -- | The sort 𝖯𝗋𝗈𝗉 intends to be the type of logical propositions.
  SortProp  |
  -- | The sort 𝖲𝖯𝗋𝗈𝗉 is like 𝖯𝗋𝗈𝗉 but the propositions in 𝖲𝖯𝗋𝗈𝗉 are known to have irrelevant proofs (all proofs are equal).
  SortSProp  |
  SortType  |
  SortTypeWithAnyUniverse  |
  SortTypeWithUniverse Universe
  deriving (Eq, Ord, Read, Show)

_Sort = Core.Name "hydra.coq.syntax.Sort"

_Sort_set = Core.Name "set"

_Sort_prop = Core.Name "prop"

_Sort_sProp = Core.Name "sProp"

_Sort_type = Core.Name "type"

_Sort_typeWithAnyUniverse = Core.Name "typeWithAnyUniverse"

_Sort_typeWithUniverse = Core.Name "typeWithUniverse"

newtype String_ =
  String_ {
    unString :: String}
  deriving (Eq, Ord, Read, Show)

_String = Core.Name "hydra.coq.syntax.String"

data Term =
  TermForallOrFun ForallOrFun |
  TermLet Let |
  TermIf If |
  TermFix Fix |
  TermCofix Cofix |
  TermTerm100 Term100
  deriving (Eq, Ord, Read, Show)

_Term = Core.Name "hydra.coq.syntax.Term"

_Term_forallOrFun = Core.Name "forallOrFun"

_Term_let = Core.Name "let"

_Term_if = Core.Name "if"

_Term_fix = Core.Name "fix"

_Term_cofix = Core.Name "cofix"

_Term_term100 = Core.Name "term100"

data Term0 =
  Term0QualidAnnotated QualidAnnotated |
  Term0Sort Sort |
  Term0PrimitiveNotations PrimitiveNotations |
  Term0Evar ExistentialVariable |
  Term0Match Match |
  Term0Record  |
  Term0Generalizing  |
  Term0Ltac  |
  Term0Parens Term
  deriving (Eq, Ord, Read, Show)

_Term0 = Core.Name "hydra.coq.syntax.Term0"

_Term0_qualidAnnotated = Core.Name "qualidAnnotated"

_Term0_sort = Core.Name "sort"

_Term0_primitiveNotations = Core.Name "primitiveNotations"

_Term0_evar = Core.Name "evar"

_Term0_match = Core.Name "match"

_Term0_record = Core.Name "record"

_Term0_generalizing = Core.Name "generalizing"

_Term0_ltac = Core.Name "ltac"

_Term0_parens = Core.Name "parens"

data Term1 =
  Term1Projection  |
  Term1Scope  |
  Term1Term0 Term0
  deriving (Eq, Ord, Read, Show)

_Term1 = Core.Name "hydra.coq.syntax.Term1"

_Term1_projection = Core.Name "projection"

_Term1_scope = Core.Name "scope"

_Term1_term0 = Core.Name "term0"

data Term10 =
  Term10Application Application |
  Term10OneTerm OneTerm
  deriving (Eq, Ord, Read, Show)

_Term10 = Core.Name "hydra.coq.syntax.Term10"

_Term10_application = Core.Name "application"

_Term10_oneTerm = Core.Name "oneTerm"

data Term100 =
  Term100Cast TypeCast |
  Term100Term10 Term10
  deriving (Eq, Ord, Read, Show)

_Term100 = Core.Name "hydra.coq.syntax.Term100"

_Term100_cast = Core.Name "cast"

_Term100_term10 = Core.Name "term10"

newtype Type =
  Type {
    unType :: Term}
  deriving (Eq, Ord, Read, Show)

_Type = Core.Name "hydra.coq.syntax.Type"

data TypeCast =
  TypeCast {
    typeCastTerm :: Term10,
    typeCastType :: Type,
    typeCastOperator :: TypeCastOperator}
  deriving (Eq, Ord, Read, Show)

_TypeCast = Core.Name "hydra.coq.syntax.TypeCast"

_TypeCast_term = Core.Name "term"

_TypeCast_type = Core.Name "type"

_TypeCast_operator = Core.Name "operator"

data TypeCastOperator =
  -- | The expression term10 : type is a type cast expression. It enforces the type of term10 to be type.
  TypeCastOperatorNormal  |
  -- | term10 <: type specifies that the virtual machine will be used to type check that term10 has type type (see vm_compute).
  TypeCastOperatorVmCompute  |
  -- | term10 <<: type specifies that compilation to OCaml will be used to type check that term10 has type type (see native_compute).
  TypeCastOperatorNativeCompute
  deriving (Eq, Ord, Read, Show)

_TypeCastOperator = Core.Name "hydra.coq.syntax.TypeCastOperator"

_TypeCastOperator_normal = Core.Name "normal"

_TypeCastOperator_vmCompute = Core.Name "vmCompute"

_TypeCastOperator_nativeCompute = Core.Name "nativeCompute"

data TypeBinders =
  TypeBinders {
    typeBindersNames :: [Name],
    typeBindersType :: Type}
  deriving (Eq, Ord, Read, Show)

_TypeBinders = Core.Name "hydra.coq.syntax.TypeBinders"

_TypeBinders_names = Core.Name "names"

_TypeBinders_type = Core.Name "type"

data TypeclassConstraint =
  TypeclassConstraint {
    typeclassConstraintName :: (Maybe Name),
    typeclassConstraintGeneralizing :: Bool,
    typeclassConstraintTerm :: Term}
  deriving (Eq, Ord, Read, Show)

_TypeclassConstraint = Core.Name "hydra.coq.syntax.TypeclassConstraint"

_TypeclassConstraint_name = Core.Name "name"

_TypeclassConstraint_generalizing = Core.Name "generalizing"

_TypeclassConstraint_term = Core.Name "term"

newtype UnivAnnot =
  UnivAnnot {
    unUnivAnnot :: [UniverseLevel]}
  deriving (Eq, Ord, Read, Show)

_UnivAnnot = Core.Name "hydra.coq.syntax.UnivAnnot"

data Universe =
  UniverseMax [Universe_Expr] |
  UniverseExpr Universe_Expr
  deriving (Eq, Ord, Read, Show)

_Universe = Core.Name "hydra.coq.syntax.Universe"

_Universe_max = Core.Name "max"

_Universe_expr = Core.Name "expr"

data Universe_Expr =
  Universe_Expr {
    universe_ExprName :: UniverseName,
    universe_ExprNumber :: (Maybe Natural)}
  deriving (Eq, Ord, Read, Show)

_Universe_Expr = Core.Name "hydra.coq.syntax.Universe_Expr"

_Universe_Expr_name = Core.Name "name"

_Universe_Expr_number = Core.Name "number"

data UniverseLevel =
  UniverseLevelSet  |
  UniverseLevelProp  |
  UniverseLevelType  |
  UniverseLevelIgnored  |
  UniverseLevelQualid Qualid
  deriving (Eq, Ord, Read, Show)

_UniverseLevel = Core.Name "hydra.coq.syntax.UniverseLevel"

_UniverseLevel_set = Core.Name "set"

_UniverseLevel_prop = Core.Name "prop"

_UniverseLevel_type = Core.Name "type"

_UniverseLevel_ignored = Core.Name "ignored"

_UniverseLevel_qualid = Core.Name "qualid"

data UniverseName =
  UniverseNameQualid Qualid |
  UniverseNameSet  |
  UniverseNameProp
  deriving (Eq, Ord, Read, Show)

_UniverseName = Core.Name "hydra.coq.syntax.UniverseName"

_UniverseName_qualid = Core.Name "qualid"

_UniverseName_set = Core.Name "set"

_UniverseName_prop = Core.Name "prop"

-- | An Axiom declaration: `Axiom <name> : <type>.`
data AxiomDeclaration =
  AxiomDeclaration {
    axiomDeclarationName :: Ident,
    axiomDeclarationType :: Type}
  deriving (Eq, Ord, Read, Show)

_AxiomDeclaration = Core.Name "hydra.coq.syntax.AxiomDeclaration"

_AxiomDeclaration_name = Core.Name "name"

_AxiomDeclaration_type = Core.Name "type"

-- | A Coq comment (* ... *)
newtype Comment =
  Comment {
    unComment :: String}
  deriving (Eq, Ord, Read, Show)

_Comment = Core.Name "hydra.coq.syntax.Comment"

-- | A constructor in an Inductive definition
data Constructor =
  Constructor {
    constructorName :: Ident,
    constructorBinders :: [Binder],
    constructorType :: (Maybe Type)}
  deriving (Eq, Ord, Read, Show)

_Constructor = Core.Name "hydra.coq.syntax.Constructor"

_Constructor_name = Core.Name "name"

_Constructor_binders = Core.Name "binders"

_Constructor_type = Core.Name "type"

-- | A Definition or Let command: Definition name binders : type := term.
data Definition =
  Definition {
    definitionLocality :: (Maybe Locality),
    definitionName :: Ident,
    definitionBinders :: [Binder],
    definitionType :: (Maybe Type),
    definitionBody :: Term}
  deriving (Eq, Ord, Read, Show)

_Definition = Core.Name "hydra.coq.syntax.Definition"

_Definition_locality = Core.Name "locality"

_Definition_name = Core.Name "name"

_Definition_binders = Core.Name "binders"

_Definition_type = Core.Name "type"

_Definition_body = Core.Name "body"

-- | A complete Coq .v file
data Document =
  Document {
    documentSentences :: [Sentence]}
  deriving (Eq, Ord, Read, Show)

_Document = Core.Name "hydra.coq.syntax.Document"

_Document_sentences = Core.Name "sentences"

-- | A Fixpoint command for recursive definitions
data FixpointDefinition =
  FixpointDefinition {
    fixpointDefinitionLocality :: (Maybe Locality),
    fixpointDefinitionName :: Ident,
    fixpointDefinitionBinders :: [Binder],
    fixpointDefinitionAnnot :: (Maybe FixAnnot),
    fixpointDefinitionType :: (Maybe Type),
    fixpointDefinitionBody :: Term,
    fixpointDefinitionWith :: [Fix_Decl]}
  deriving (Eq, Ord, Read, Show)

_FixpointDefinition = Core.Name "hydra.coq.syntax.FixpointDefinition"

_FixpointDefinition_locality = Core.Name "locality"

_FixpointDefinition_name = Core.Name "name"

_FixpointDefinition_binders = Core.Name "binders"

_FixpointDefinition_annot = Core.Name "annot"

_FixpointDefinition_type = Core.Name "type"

_FixpointDefinition_body = Core.Name "body"

_FixpointDefinition_with = Core.Name "with"

-- | Qualification for Require/Import commands
data ImportQualification =
  ImportQualificationImport  |
  ImportQualificationExport
  deriving (Eq, Ord, Read, Show)

_ImportQualification = Core.Name "hydra.coq.syntax.ImportQualification"

_ImportQualification_import = Core.Name "import"

_ImportQualification_export = Core.Name "export"

-- | A single body in an Inductive definition (supports mutual induction via 'with')
data InductiveBody =
  InductiveBody {
    inductiveBodyName :: Ident,
    inductiveBodyBinders :: [Binder],
    inductiveBodyType :: (Maybe Type),
    inductiveBodyConstructors :: [Constructor]}
  deriving (Eq, Ord, Read, Show)

_InductiveBody = Core.Name "hydra.coq.syntax.InductiveBody"

_InductiveBody_name = Core.Name "name"

_InductiveBody_binders = Core.Name "binders"

_InductiveBody_type = Core.Name "type"

_InductiveBody_constructors = Core.Name "constructors"

-- | An Inductive or CoInductive definition with one or more mutually inductive bodies
data InductiveDefinition =
  InductiveDefinition {
    inductiveDefinitionLocality :: (Maybe Locality),
    inductiveDefinitionCoinductive :: Bool,
    inductiveDefinitionBodies :: [InductiveBody]}
  deriving (Eq, Ord, Read, Show)

_InductiveDefinition = Core.Name "hydra.coq.syntax.InductiveDefinition"

_InductiveDefinition_locality = Core.Name "locality"

_InductiveDefinition_coinductive = Core.Name "coinductive"

_InductiveDefinition_bodies = Core.Name "bodies"

-- | Local or Global qualifier for commands
data Locality =
  LocalityLocal  |
  LocalityGlobal
  deriving (Eq, Ord, Read, Show)

_Locality = Core.Name "hydra.coq.syntax.Locality"

_Locality_local = Core.Name "local"

_Locality_global = Core.Name "global"

-- | A Module ... End block
data ModuleDefinition =
  ModuleDefinition {
    moduleDefinitionName :: Ident,
    moduleDefinitionSentences :: [Sentence]}
  deriving (Eq, Ord, Read, Show)

_ModuleDefinition = Core.Name "hydra.coq.syntax.ModuleDefinition"

_ModuleDefinition_name = Core.Name "name"

_ModuleDefinition_sentences = Core.Name "sentences"

-- | A Notation declaration
data NotationDeclaration =
  NotationDeclaration {
    notationDeclarationNotation :: String_,
    notationDeclarationDefinition :: Term,
    notationDeclarationLevel :: (Maybe Natural),
    notationDeclarationAssociativity :: (Maybe String)}
  deriving (Eq, Ord, Read, Show)

_NotationDeclaration = Core.Name "hydra.coq.syntax.NotationDeclaration"

_NotationDeclaration_notation = Core.Name "notation"

_NotationDeclaration_definition = Core.Name "definition"

_NotationDeclaration_level = Core.Name "level"

_NotationDeclaration_associativity = Core.Name "associativity"

-- | The body of a Record definition
data RecordBody =
  RecordBody {
    recordBodyConstructor :: (Maybe Ident),
    recordBodyFields :: [RecordField]}
  deriving (Eq, Ord, Read, Show)

_RecordBody = Core.Name "hydra.coq.syntax.RecordBody"

_RecordBody_constructor = Core.Name "constructor"

_RecordBody_fields = Core.Name "fields"

-- | A Record or Structure definition
data RecordDefinition =
  RecordDefinition {
    recordDefinitionLocality :: (Maybe Locality),
    recordDefinitionName :: Ident,
    recordDefinitionBinders :: [Binder],
    recordDefinitionSort :: (Maybe Sort),
    recordDefinitionBody :: RecordBody}
  deriving (Eq, Ord, Read, Show)

_RecordDefinition = Core.Name "hydra.coq.syntax.RecordDefinition"

_RecordDefinition_locality = Core.Name "locality"

_RecordDefinition_name = Core.Name "name"

_RecordDefinition_binders = Core.Name "binders"

_RecordDefinition_sort = Core.Name "sort"

_RecordDefinition_body = Core.Name "body"

-- | A field in a Record definition
data RecordField =
  RecordField {
    recordFieldName :: Ident,
    recordFieldType :: Type}
  deriving (Eq, Ord, Read, Show)

_RecordField = Core.Name "hydra.coq.syntax.RecordField"

_RecordField_name = Core.Name "name"

_RecordField_type = Core.Name "type"

-- | A Require Import/Export command
data RequireImport =
  RequireImport {
    requireImportFrom :: (Maybe Qualid),
    requireImportRequire :: Bool,
    requireImportQualification :: (Maybe ImportQualification),
    requireImportModules :: [Qualid]}
  deriving (Eq, Ord, Read, Show)

_RequireImport = Core.Name "hydra.coq.syntax.RequireImport"

_RequireImport_from = Core.Name "from"

_RequireImport_require = Core.Name "require"

_RequireImport_qualification = Core.Name "qualification"

_RequireImport_modules = Core.Name "modules"

-- | A Section ... End block
data SectionDefinition =
  SectionDefinition {
    sectionDefinitionName :: Ident,
    sectionDefinitionSentences :: [Sentence]}
  deriving (Eq, Ord, Read, Show)

_SectionDefinition = Core.Name "hydra.coq.syntax.SectionDefinition"

_SectionDefinition_name = Core.Name "name"

_SectionDefinition_sentences = Core.Name "sentences"

-- | A top-level sentence in a Coq document, optionally preceded by a comment
data Sentence =
  Sentence {
    sentenceComment :: (Maybe Comment),
    sentenceContent :: SentenceContent}
  deriving (Eq, Ord, Read, Show)

_Sentence = Core.Name "hydra.coq.syntax.Sentence"

_Sentence_comment = Core.Name "comment"

_Sentence_content = Core.Name "content"

-- | The content of a top-level sentence
data SentenceContent =
  SentenceContentAxiom AxiomDeclaration |
  SentenceContentDefinition Definition |
  SentenceContentFixpoint FixpointDefinition |
  SentenceContentInductive InductiveDefinition |
  SentenceContentModule ModuleDefinition |
  SentenceContentNotation NotationDeclaration |
  SentenceContentRecord RecordDefinition |
  SentenceContentRequireImport RequireImport |
  SentenceContentSection SectionDefinition |
  SentenceContentTheorem TheoremBody
  deriving (Eq, Ord, Read, Show)

_SentenceContent = Core.Name "hydra.coq.syntax.SentenceContent"

_SentenceContent_axiom = Core.Name "axiom"

_SentenceContent_definition = Core.Name "definition"

_SentenceContent_fixpoint = Core.Name "fixpoint"

_SentenceContent_inductive = Core.Name "inductive"

_SentenceContent_module = Core.Name "module"

_SentenceContent_notation = Core.Name "notation"

_SentenceContent_record = Core.Name "record"

_SentenceContent_requireImport = Core.Name "requireImport"

_SentenceContent_section = Core.Name "section"

_SentenceContent_theorem = Core.Name "theorem"

-- | A Theorem/Lemma/Proposition with a proof term
data TheoremBody =
  TheoremBody {
    theoremBodyKind :: TheoremKind,
    theoremBodyName :: Ident,
    theoremBodyBinders :: [Binder],
    theoremBodyType :: Type,
    theoremBodyProof :: Term}
  deriving (Eq, Ord, Read, Show)

_TheoremBody = Core.Name "hydra.coq.syntax.TheoremBody"

_TheoremBody_kind = Core.Name "kind"

_TheoremBody_name = Core.Name "name"

_TheoremBody_binders = Core.Name "binders"

_TheoremBody_type = Core.Name "type"

_TheoremBody_proof = Core.Name "proof"

-- | The kind of theorem command
data TheoremKind =
  TheoremKindTheorem  |
  TheoremKindLemma  |
  TheoremKindProposition  |
  TheoremKindCorollary  |
  TheoremKindExample
  deriving (Eq, Ord, Read, Show)

_TheoremKind = Core.Name "hydra.coq.syntax.TheoremKind"

_TheoremKind_theorem = Core.Name "theorem"

_TheoremKind_lemma = Core.Name "lemma"

_TheoremKind_proposition = Core.Name "proposition"

_TheoremKind_corollary = Core.Name "corollary"

_TheoremKind_example = Core.Name "example"