inductive Foo where
  | a | b | c

def f : Foo → Nat
  | Foo.a => 10
  | Foo.b => 20
  | Foo.c => 35

inductive CXCursorKind where
  | CXCursor_UnexposedDecl
  | CXCursor_StructDecl
  | CXCursor_UnionDecl
  | CXCursor_ClassDecl
  | CXCursor_EnumDecl
  | CXCursor_FieldDecl
  | CXCursor_EnumConstantDecl
  | CXCursor_FunctionDecl
  | CXCursor_VarDecl
  | CXCursor_ParmDecl
  | CXCursor_ObjCInterfaceDecl
  | CXCursor_ObjCCategoryDecl
  | CXCursor_ObjCProtocolDecl
  | CXCursor_ObjCPropertyDecl
  | CXCursor_ObjCIvarDecl
  | CXCursor_ObjCInstanceMethodDecl
  | CXCursor_ObjCClassMethodDecl
  | CXCursor_ObjCImplementationDecl
  | CXCursor_ObjCCategoryImplDecl
  | CXCursor_TypedefDecl
  | CXCursor_CXXMethod
  | CXCursor_Namespace
  | CXCursor_LinkageSpec
  | CXCursor_Constructor
  | CXCursor_Destructor
  | CXCursor_ConversionFunction
  | CXCursor_TemplateTypeParameter
  | CXCursor_NonTypeTemplateParameter
  | CXCursor_TemplateTemplateParameter
  | CXCursor_FunctionTemplate
  | CXCursor_ClassTemplate
  | CXCursor_ClassTemplatePartialSpecialization
  | CXCursor_NamespaceAlias
  | CXCursor_UsingDirective
  | CXCursor_UsingDeclaration
  | CXCursor_TypeAliasDecl
  | CXCursor_ObjCSynthesizeDecl
  | CXCursor_ObjCDynamicDecl
  | CXCursor_CXXAccessSpecifier
  | CXCursor_FirstDecl
  | CXCursor_LastDecl
  | CXCursor_FirstRef
  | CXCursor_ObjCSuperClassRef
  | CXCursor_ObjCProtocolRef
  | CXCursor_ObjCClassRef
  | CXCursor_TypeRef
  | CXCursor_CXXBaseSpecifier
  | CXCursor_TemplateRef
  | CXCursor_NamespaceRef
  | CXCursor_MemberRef
  | CXCursor_LabelRef
  | CXCursor_OverloadedDeclRef
  | CXCursor_VariableRef
  | CXCursor_LastRef
  | CXCursor_FirstInvalid
  | CXCursor_InvalidFile
  | CXCursor_NoDeclFound
  | CXCursor_NotImplemented
  | CXCursor_InvalidCode
  | CXCursor_LastInvalid
  | CXCursor_FirstExpr
  | CXCursor_UnexposedExpr
  | CXCursor_DeclRefExpr
  | CXCursor_MemberRefExpr
  | CXCursor_CallExpr
  | CXCursor_ObjCMessageExpr
  | CXCursor_BlockExpr
  | CXCursor_IntegerLiteral
  | CXCursor_FloatingLiteral
  | CXCursor_ImaginaryLiteral
  | CXCursor_StringLiteral
  | CXCursor_CharacterLiteral
  | CXCursor_ParenExpr
  | CXCursor_UnaryOperator
  | CXCursor_ArraySubscriptExpr
  | CXCursor_BinaryOperator
  | CXCursor_CompoundAssignOperator
  | CXCursor_ConditionalOperator
  | CXCursor_CStyleCastExpr
  | CXCursor_CompoundLiteralExpr
  | CXCursor_InitListExpr
  | CXCursor_AddrLabelExpr
  | CXCursor_StmtExpr
  | CXCursor_GenericSelectionExpr
  | CXCursor_GNUNullExpr
  | CXCursor_CXXStaticCastExpr
  | CXCursor_CXXDynamicCastExpr
  | CXCursor_CXXReinterpretCastExpr
  | CXCursor_CXXConstCastExpr
  | CXCursor_CXXFunctionalCastExpr
  | CXCursor_CXXTypeidExpr
  | CXCursor_CXXBoolLiteralExpr
  | CXCursor_CXXNullPtrLiteralExpr
  | CXCursor_CXXThisExpr
  | CXCursor_CXXThrowExpr
  | CXCursor_CXXNewExpr
  | CXCursor_CXXDeleteExpr
  | CXCursor_UnaryExpr
  | CXCursor_ObjCStringLiteral
  | CXCursor_ObjCEncodeExpr
  | CXCursor_ObjCSelectorExpr
  | CXCursor_ObjCProtocolExpr
  | CXCursor_ObjCBridgedCastExpr
  | CXCursor_PackExpansionExpr
  | CXCursor_SizeOfPackExpr
  | CXCursor_LambdaExpr
  | CXCursor_ObjCBoolLiteralExpr
  | CXCursor_ObjCSelfExpr
  | CXCursor_OMPArraySectionExpr
  | CXCursor_ObjCAvailabilityCheckExpr
  | CXCursor_FixedPointLiteral
  | CXCursor_OMPArrayShapingExpr
  | CXCursor_OMPIteratorExpr
  | CXCursor_CXXAddrspaceCastExpr
  | CXCursor_LastExpr
  | CXCursor_FirstStmt
  | CXCursor_UnexposedStmt
  | CXCursor_LabelStmt
  | CXCursor_CompoundStmt
  | CXCursor_CaseStmt
  | CXCursor_DefaultStmt
  | CXCursor_IfStmt
  | CXCursor_SwitchStmt
  | CXCursor_WhileStmt
  | CXCursor_DoStmt
  | CXCursor_ForStmt
  | CXCursor_GotoStmt
  | CXCursor_IndirectGotoStmt
  | CXCursor_ContinueStmt
  | CXCursor_BreakStmt
  | CXCursor_ReturnStmt
  | CXCursor_GCCAsmStmt
  | CXCursor_AsmStmt
  | CXCursor_ObjCAtTryStmt
  | CXCursor_ObjCAtCatchStmt
  | CXCursor_ObjCAtFinallyStmt
  | CXCursor_ObjCAtThrowStmt
  | CXCursor_ObjCAtSynchronizedStmt
  | CXCursor_ObjCAutoreleasePoolStmt
  | CXCursor_ObjCForCollectionStmt
  | CXCursor_CXXCatchStmt
  | CXCursor_CXXTryStmt
  | CXCursor_CXXForRangeStmt
  | CXCursor_SEHTryStmt
  | CXCursor_SEHExceptStmt
  | CXCursor_SEHFinallyStmt
  | CXCursor_MSAsmStmt
  | CXCursor_NullStmt
  | CXCursor_DeclStmt
  | CXCursor_OMPParallelDirective
  | CXCursor_OMPSimdDirective
  | CXCursor_OMPForDirective
  | CXCursor_OMPSectionsDirective
  | CXCursor_OMPSectionDirective
  | CXCursor_OMPSingleDirective
  | CXCursor_OMPParallelForDirective
  | CXCursor_OMPParallelSectionsDirective
  | CXCursor_OMPTaskDirective
  | CXCursor_OMPMasterDirective
  | CXCursor_OMPCriticalDirective
  | CXCursor_OMPTaskyieldDirective
  | CXCursor_OMPBarrierDirective
  | CXCursor_OMPTaskwaitDirective
  | CXCursor_OMPFlushDirective
  | CXCursor_SEHLeaveStmt
  | CXCursor_OMPOrderedDirective
  | CXCursor_OMPAtomicDirective
  | CXCursor_OMPForSimdDirective
  | CXCursor_OMPParallelForSimdDirective
  | CXCursor_OMPTargetDirective
  | CXCursor_OMPTeamsDirective
  | CXCursor_OMPTaskgroupDirective
  | CXCursor_OMPCancellationPointDirective
  | CXCursor_OMPCancelDirective
  | CXCursor_OMPTargetDataDirective
  | CXCursor_OMPTaskLoopDirective
  | CXCursor_OMPTaskLoopSimdDirective
  | CXCursor_OMPDistributeDirective
  | CXCursor_OMPTargetEnterDataDirective
  | CXCursor_OMPTargetExitDataDirective
  | CXCursor_OMPTargetParallelDirective
  | CXCursor_OMPTargetParallelForDirective
  | CXCursor_OMPTargetUpdateDirective
  | CXCursor_OMPDistributeParallelForDirective
  | CXCursor_OMPDistributeParallelForSimdDirective
  | CXCursor_OMPDistributeSimdDirective
  | CXCursor_OMPTargetParallelForSimdDirective
  | CXCursor_OMPTargetSimdDirective
  | CXCursor_OMPTeamsDistributeDirective
  | CXCursor_OMPTeamsDistributeSimdDirective
  | CXCursor_OMPTeamsDistributeParallelForSimdDirective
  | CXCursor_OMPTeamsDistributeParallelForDirective
  | CXCursor_OMPTargetTeamsDirective
  | CXCursor_OMPTargetTeamsDistributeDirective
  | CXCursor_OMPTargetTeamsDistributeParallelForDirective
  | CXCursor_OMPTargetTeamsDistributeParallelForSimdDirective
  | CXCursor_OMPTargetTeamsDistributeSimdDirective
  | CXCursor_BuiltinBitCastExpr
  | CXCursor_OMPMasterTaskLoopDirective
  | CXCursor_OMPParallelMasterTaskLoopDirective
  | CXCursor_OMPMasterTaskLoopSimdDirective
  | CXCursor_OMPParallelMasterTaskLoopSimdDirective
  | CXCursor_OMPParallelMasterDirective
  | CXCursor_OMPDepobjDirective
  | CXCursor_OMPScanDirective
  | CXCursor_OMPTileDirective
  | CXCursor_OMPCanonicalLoop
  | CXCursor_OMPInteropDirective
  | CXCursor_OMPDispatchDirective
  | CXCursor_OMPMaskedDirective
  | CXCursor_OMPUnrollDirective
  | CXCursor_LastStmt
  | CXCursor_TranslationUnit
  | CXCursor_FirstAttr
  | CXCursor_UnexposedAttr
  | CXCursor_IBActionAttr
  | CXCursor_IBOutletAttr
  | CXCursor_IBOutletCollectionAttr
  | CXCursor_CXXFinalAttr
  | CXCursor_CXXOverrideAttr
  | CXCursor_AnnotateAttr
  | CXCursor_AsmLabelAttr
  | CXCursor_PackedAttr
  | CXCursor_PureAttr
  | CXCursor_ConstAttr
  | CXCursor_NoDuplicateAttr
  | CXCursor_CUDAConstantAttr
  | CXCursor_CUDADeviceAttr
  | CXCursor_CUDAGlobalAttr
  | CXCursor_CUDAHostAttr
  | CXCursor_CUDASharedAttr
  | CXCursor_VisibilityAttr
  | CXCursor_DLLExport
  | CXCursor_DLLImport
  | CXCursor_NSReturnsRetained
  | CXCursor_NSReturnsNotRetained
  | CXCursor_NSReturnsAutoreleased
  | CXCursor_NSConsumesSelf
  | CXCursor_NSConsumed
  | CXCursor_ObjCException
  | CXCursor_ObjCNSObject
  | CXCursor_ObjCIndependentClass
  | CXCursor_ObjCPreciseLifetime
  | CXCursor_ObjCReturnsInnerPointer
  | CXCursor_ObjCRequiresSuper
  | CXCursor_ObjCRootClass
  | CXCursor_ObjCSubclassingRestricted
  | CXCursor_ObjCExplicitProtocolImpl
  | CXCursor_ObjCDesignatedInitializer
  | CXCursor_ObjCRuntimeVisible
  | CXCursor_ObjCBoxable
  | CXCursor_FlagEnum
  | CXCursor_ConvergentAttr
  | CXCursor_WarnUnusedAttr
  | CXCursor_WarnUnusedResultAttr
  | CXCursor_AlignedAttr
  | CXCursor_LastAttr
  | CXCursor_PreprocessingDirective
  | CXCursor_MacroDefinition
  | CXCursor_MacroExpansion
  | CXCursor_MacroInstantiation
  | CXCursor_InclusionDirective
  | CXCursor_FirstPreprocessing
  | CXCursor_LastPreprocessing
  | CXCursor_ModuleImportDecl
  | CXCursor_TypeAliasTemplateDecl
  | CXCursor_StaticAssert
  | CXCursor_FriendDecl
  | CXCursor_FirstExtraDecl
  | CXCursor_LastExtraDecl
  | CXCursor_OverloadCandidate
  deriving BEq, DecidableEq

open CXCursorKind

example (h : CXCursor_CUDAGlobalAttr = CXCursor_CUDAHostAttr) : False := by
  contradiction

/-- info: false -/
#guard_msgs in
#eval CXCursor_CUDAGlobalAttr == CXCursor_CUDAHostAttr

/-- info: false -/
#guard_msgs in
#eval decide (CXCursor_CUDAGlobalAttr = CXCursor_CUDAHostAttr)