HORIZON HASKELLDocslts/ghc-9.14.x3e2d5682026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 3e2d568 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Translation.ConcreteToAbstract

Translation from Agda.Syntax.Concrete to Agda.Syntax.Abstract. Involves scope analysis, figuring out infix operator precedences and tidying up definitions.

  • 2 types
  • 1 class
  • 6 values
  • PackageAgda-2.8.0.2
  • Exports9
  • LanguageHaskell2010
  • LicenceMIT
  • SourceConcreteToAbstract.hs
classclass ToAbstract c where
#

Things that can be translated to abstract syntax are instances of this class.

Associated types

Methods

Instances51ToAbstract, …
  • ToAbstract ExprDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Scope check an expression.

  • ToAbstract HoleContentDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Content of interaction hole.

  • ToAbstract LHSCoreDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Scope-check a LHSCore not of a C.DisplayForm.

  • ToAbstract LamBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract ModuleAssignmentDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract PatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Scope check a Pattern not belonging to a C.DisplayForm.

  • ToAbstract PragmaDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract RHSDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract RewriteEqnDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract TypedBindingDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract ClauseDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract NiceDeclarationDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract AbstractRHSDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract CLHSCoreDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract CPatternDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract DataConstrDeclDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract DeclarationsDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract GenTelDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract GenTelAndTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract LeftHandSideDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract LetDefDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract LetDefsDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract MaybeOldQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract NewModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract NewModuleQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract OldModuleNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract OldQNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract PatNameDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract RecordConstructorTypeDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract RightHandSideDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract ()Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract (LHSCore' Expr)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract (Pattern' Expr)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract (Binder' (NewName BoundName))Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract (NewName BoundName)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract (NewName Name)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract (TopLevel [Declaration])Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

  • ToAbstract (WithHidingInfo Pattern)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Hiding info is only used for pattern variables.

  • ToAbstract c => ToAbstract (Arg c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract c => ToAbstract (Ranged c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract c => ToAbstract (WithHiding c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract c => ToAbstract (FieldAssignment' c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract c => ToAbstract (List1 c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract c => ToAbstract (Maybe c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract c => ToAbstract [c]Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToQName a => ToAbstract (OldName a)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Should be a defined name.

  • ToAbstract c => ToAbstract (Named name c)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • (ToAbstract c1, ToAbstract c2) => ToAbstract (Either c1 c2)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • (ToAbstract c1, ToAbstract c2) => ToAbstract (c1, c2)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • (ToAbstract c1, ToAbstract c2, ToAbstract c3) => ToAbstract (c1, c2, c3)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
  • ToAbstract (RewriteEqn' () BindName Pattern Expr)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract
datadata TopLevel a
#

Temporary data type to scope check a file.

Constructors

Instances2ToAbstract, AbsOfCon
  • ToAbstract (TopLevel [Declaration])Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract

    Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

  • type AbsOfCon (TopLevel [Declaration]) = TopLevelInfoDefined in Agda-2.8.0.2 · Agda.Syntax.Translation.ConcreteToAbstract