Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Abstract

Contents

Orphan instances

Description

The abstract syntax. This is what you get after desugaring and scope analysis of the concrete syntax. The type checker works on abstract syntax, producing internal syntax (Agda.Syntax.Internal).

Synopsis

class SubstExpr a where
- substExpr :: [(Name, Expr)] -> a -> a
type PatternSynDefns = Map QName PatternSynDefn
type PatternSynDefn = ([Arg Name], Pattern' Void)
class NameToExpr a where
- nameToExpr :: a -> Expr
class AnyAbstract a where
- anyAbstract :: a -> Bool
type HoleContent = HoleContent' () BindName Pattern Expr
type Patterns = [NamedArg Pattern]
type Pattern = Pattern' Expr
type NAPs1 e = List1 (NamedArg (Pattern' e))
type NAPs e = [NamedArg (Pattern' e)]
data Pattern' e
- = VarP BindName
- | ConP ConPatInfo AmbiguousQName (NAPs e)
- | ProjP PatInfo ProjOrigin AmbiguousQName
- | DefP PatInfo AmbiguousQName (NAPs e)
- | WildP PatInfo
- | AsP PatInfo BindName (Pattern' e)
- | DotP PatInfo e
- | AbsurdP PatInfo
- | LitP PatInfo Literal
- | PatternSynP PatInfo AmbiguousQName (NAPs e)
- | RecP PatInfo [FieldAssignment' (Pattern' e)]
- | EqualP PatInfo [(e, e)]
- | WithP PatInfo (Pattern' e)
- | AnnP PatInfo e (Pattern' e)
type LHSCore = LHSCore' Expr
data LHSCore' e
- = LHSHead {
  - lhsDefName :: QName
  - lhsPats :: [NamedArg (Pattern' e)]
  }
- | LHSProj {
  - lhsDestructor :: AmbiguousQName
  - lhsFocus :: NamedArg (LHSCore' e)
  - lhsPats :: [NamedArg (Pattern' e)]
  }
- | LHSWith {
  - lhsHead :: LHSCore' e
  - lhsWithPatterns :: [Arg (Pattern' e)]
  - lhsPats :: [NamedArg (Pattern' e)]
  }
data LHS = LHS {
- lhsInfo :: LHSInfo
- lhsCore :: LHSCore
}
data SpineLHS = SpineLHS {
- spLhsInfo :: LHSInfo
- spLhsDefName :: QName
- spLhsPats :: [NamedArg Pattern]
}
data RHS
- = RHS {
  - rhsExpr :: Expr
  - rhsConcrete :: Maybe Expr
  }
- | AbsurdRHS
- | WithRHS QName [WithExpr] [Clause]
- | RewriteRHS {
  - rewriteExprs :: [RewriteEqn]
  - rewriteStrippedPats :: [ProblemEq]
  - rewriteRHS :: RHS
  - rewriteWhereDecls :: WhereDeclarations
  }
type WithExpr = WithExpr' Expr
type WithExpr' e = Named BindName (Arg e)
type RewriteEqn = RewriteEqn' QName BindName Pattern Expr
type SpineClause = Clause' SpineLHS
type Clause = Clause' LHS
data WhereDeclarations = WhereDecls {
- whereModule :: Maybe ModuleName
- whereDecls :: Maybe Declaration
}
data Clause' lhs = Clause {
- clauseLHS :: lhs
- clauseStrippedPats :: [ProblemEq]
- clauseRHS :: RHS
- clauseWhereDecls :: WhereDeclarations
- clauseCatchall :: Bool
}
data ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
}
data DataDefParams = DataDefParams {
- dataDefGeneralizedParams :: Set Name
- dataDefParams :: [LamBinding]
}
data GeneralizeTelescope = GeneralizeTel {
- generalizeTelVars :: Map QName Name
- generalizeTel :: Telescope
}
type Telescope = [TypedBinding]
type Telescope1 = List1 TypedBinding
data TypedBinding
- = TBind Range TacticAttr (List1 (NamedArg Binder)) Expr
- | TLet Range (List1 LetBinding)
data LamBinding
- = DomainFree TacticAttr (NamedArg Binder)
- | DomainFull TypedBinding
type Binder = Binder' BindName
data Binder' a = Binder {
- binderPattern :: Maybe Pattern
- binderName :: a
}
type TacticAttr = Maybe Expr
type Field = TypeSignature
type Constructor = TypeSignature
type TypeSignature = Declaration
data LetBinding
- = LetBind LetInfo ArgInfo BindName Expr Expr
- | LetPatBind LetInfo Pattern Expr
- | LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
- | LetOpen ModuleInfo ModuleName ImportDirective
- | LetDeclaredVariable BindName
data Pragma
- = OptionsPragma [String]
- | BuiltinPragma RString ResolvedName
- | BuiltinNoDefPragma RString KindOfName QName
- | RewritePragma Range [QName]
- | CompilePragma RString QName String
- | StaticPragma QName
- | EtaPragma QName
- | InjectivePragma QName
- | InlinePragma Bool QName
- | DisplayPragma QName [NamedArg Pattern] Expr
data ModuleApplication
- = SectionApp Telescope ModuleName [NamedArg Expr]
- | RecordModuleInstance ModuleName
type ImportedName = ImportedName' QName ModuleName
type Renaming = Renaming' QName ModuleName
type ImportDirective = ImportDirective' QName ModuleName
type DefInfo = DefInfo' Expr
data Declaration
- = Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Expr
- | Generalize (Set QName) DefInfo ArgInfo QName Expr
- | Field DefInfo QName (Arg Expr)
- | Primitive DefInfo QName (Arg Expr)
- | Mutual MutualInfo [Declaration]
- | Section Range ModuleName GeneralizeTelescope [Declaration]
- | Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective
- | Import ModuleInfo ModuleName ImportDirective
- | Pragma Range Pragma
- | Open ModuleInfo ModuleName ImportDirective
- | FunDef DefInfo QName Delayed [Clause]
- | DataSig DefInfo QName GeneralizeTelescope Expr
- | DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
- | RecSig DefInfo QName GeneralizeTelescope Expr
- | RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Expr [Declaration]
- | PatternSynDef QName [Arg BindName] (Pattern' Void)
- | UnquoteDecl MutualInfo [DefInfo] [QName] Expr
- | UnquoteDef [DefInfo] [QName] Expr
- | ScopedDecl ScopeInfo [Declaration]
type RecordDirectives = RecordDirectives' QName
data ScopeCopyInfo = ScopeCopyInfo {
- renModules :: Ren ModuleName
- renNames :: Ren QName
}
type Ren a = Map a (List1 a)
type RecordAssigns = [RecordAssign]
type RecordAssign = Either Assign ModuleName
type Assigns = [Assign]
type Assign = FieldAssignment' Expr
data Expr
- = Var Name
- | Def' QName Suffix
- | Proj ProjOrigin AmbiguousQName
- | Con AmbiguousQName
- | PatternSyn AmbiguousQName
- | Macro QName
- | Lit ExprInfo Literal
- | QuestionMark MetaInfo InteractionId
- | Underscore MetaInfo
- | Dot ExprInfo Expr
- | App AppInfo Expr (NamedArg Expr)
- | WithApp ExprInfo Expr [Expr]
- | Lam ExprInfo LamBinding Expr
- | AbsurdLam ExprInfo Hiding
- | ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
- | Pi ExprInfo Telescope1 Expr
- | Generalized (Set QName) Expr
- | Fun ExprInfo (Arg Expr) Expr
- | Let ExprInfo (List1 LetBinding) Expr
- | ETel Telescope
- | Rec ExprInfo RecordAssigns
- | RecUpdate ExprInfo Expr Assigns
- | ScopedExpr ScopeInfo Expr
- | Quote ExprInfo
- | QuoteTerm ExprInfo
- | Unquote ExprInfo
- | DontCare Expr
type Args = [NamedArg Expr]
newtype BindName = BindName {
- unBind :: Name
}
pattern Def :: QName -> Expr
mkBindName :: Name -> BindName
generalized :: Set QName -> Expr -> Expr
initCopyInfo :: ScopeCopyInfo
mkBinder :: a -> Binder' a
mkBinder_ :: Name -> Binder
extractPattern :: Binder' a -> Maybe (Pattern, a)
mkDomainFree :: NamedArg Binder -> LamBinding
mkTBind :: Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding
mkTLet :: Range -> [LetBinding] -> Maybe TypedBinding
mkPi :: ExprInfo -> Telescope -> Expr -> Expr
noDataDefParams :: DataDefParams
noWhereDecls :: WhereDeclarations
axiomName :: Declaration -> QName
app :: Expr -> [NamedArg Expr] -> Expr
mkLet :: ExprInfo -> [LetBinding] -> Expr -> Expr
patternToExpr :: Pattern -> Expr
lambdaLiftExpr :: [Name] -> Expr -> Expr
insertImplicitPatSynArgs :: HasRange a => (Range -> a) -> Range -> [Arg Name] -> [NamedArg a] -> Maybe ([(Name, a)], [Arg Name])
module Agda.Syntax.Abstract.Name

Documentation

class SubstExpr a where Source #

Minimal complete definition

Nothing

Methods

substExpr :: [(Name, Expr)] -> a -> a Source #

default substExpr :: (Functor t, SubstExpr b, t b ~ a) => [(Name, Expr)] -> a -> a Source #

Instances

Instances details

SubstExpr Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
SubstExpr ModuleName Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> ModuleName -> ModuleName Source #
SubstExpr Name Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name0, Expr)] -> Name -> Name Source #
SubstExpr a => SubstExpr (Arg a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Arg a -> Arg a Source #
SubstExpr a => SubstExpr (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source #
SubstExpr a => SubstExpr (List1 a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> List1 a -> List1 a Source #
SubstExpr a => SubstExpr (Maybe a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Maybe a -> Maybe a Source #
SubstExpr a => SubstExpr [a] Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> [a] -> [a] Source #
SubstExpr a => SubstExpr (Named name a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Named name a -> Named name a Source #
(SubstExpr a, SubstExpr b) => SubstExpr (Either a b) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Either a b -> Either a b Source #
(SubstExpr a, SubstExpr b) => SubstExpr (a, b) Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> (a, b) -> (a, b) Source #

type PatternSynDefns = Map QName PatternSynDefn Source #

type PatternSynDefn = ([Arg Name], Pattern' Void) Source #

class NameToExpr a where Source #

Turn a name into an expression.

Methods

nameToExpr :: a -> Expr Source #

Instances

Instances details

NameToExpr AbstractName Source #	Turn an `AbstractName` into an expression.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: AbstractName -> Expr Source #
NameToExpr ResolvedName Source #	Turn a `ResolvedName` into an expression. Assumes name is not `UnknownName`.
Instance details Defined in Agda.Syntax.Abstract Methods nameToExpr :: ResolvedName -> Expr Source #

class AnyAbstract a where Source #

Are we in an abstract block?

In that case some definition is abstract.

Methods

anyAbstract :: a -> Bool Source #

Instances

Instances details

AnyAbstract Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
AnyAbstract a => AnyAbstract [a] Source #
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: [a] -> Bool Source #

type HoleContent = HoleContent' () BindName Pattern Expr Source #

type Patterns = [NamedArg Pattern] Source #

type Pattern = Pattern' Expr Source #

type NAPs1 e = List1 (NamedArg (Pattern' e)) Source #

type NAPs e = [NamedArg (Pattern' e)] Source #

data Pattern' e Source #

Parameterised over the type of dot patterns.

Constructors

VarP BindName
ConP ConPatInfo AmbiguousQName (NAPs e)
ProjP PatInfo ProjOrigin AmbiguousQName	Destructor pattern `d`.
DefP PatInfo AmbiguousQName (NAPs e)	Defined pattern: function definition `f ps`. It is also abused to convert destructor patterns into concrete syntax thus, we put AmbiguousQName here as well.
WildP PatInfo	Underscore pattern entered by user. Or generated at type checking for implicit arguments.
AsP PatInfo BindName (Pattern' e)
DotP PatInfo e	Dot pattern `.e`
AbsurdP PatInfo
LitP PatInfo Literal
PatternSynP PatInfo AmbiguousQName (NAPs e)
RecP PatInfo [FieldAssignment' (Pattern' e)]
EqualP PatInfo [(e, e)]
WithP PatInfo (Pattern' e)	`\| p`, for with-patterns.
AnnP PatInfo e (Pattern' e)	Pattern with type annotation

Instances

Instances details

MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
ToConcrete Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Pattern Source # Methods toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern) Source # bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b Source #
IsFlexiblePattern Pattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #
Foldable Pattern' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => Pattern' m -> m # foldMap :: Monoid m => (a -> m) -> Pattern' a -> m # foldMap' :: Monoid m => (a -> m) -> Pattern' a -> m # foldr :: (a -> b -> b) -> b -> Pattern' a -> b # foldr' :: (a -> b -> b) -> b -> Pattern' a -> b # foldl :: (b -> a -> b) -> b -> Pattern' a -> b # foldl' :: (b -> a -> b) -> b -> Pattern' a -> b # foldr1 :: (a -> a -> a) -> Pattern' a -> a # foldl1 :: (a -> a -> a) -> Pattern' a -> a # toList :: Pattern' a -> [a] # null :: Pattern' a -> Bool # length :: Pattern' a -> Int # elem :: Eq a => a -> Pattern' a -> Bool # maximum :: Ord a => Pattern' a -> a # minimum :: Ord a => Pattern' a -> a # sum :: Num a => Pattern' a -> a # product :: Num a => Pattern' a -> a #
Traversable Pattern' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Pattern' a -> f (Pattern' b) # sequenceA :: Applicative f => Pattern' (f a) -> f (Pattern' a) # mapM :: Monad m => (a -> m b) -> Pattern' a -> m (Pattern' b) # sequence :: Monad m => Pattern' (m a) -> m (Pattern' a) #
Functor Pattern' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b # (<$) :: a -> Pattern' b -> Pattern' a #
IsProjP (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Pattern' e -> Maybe (ProjOrigin, AmbiguousQName) Source #
APatternLike (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Associated Types type ADotT (Pattern' a) Source # Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Pattern' a)) -> m -> m) -> Pattern' a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> (Pattern' (ADotT (Pattern' a)) -> m (Pattern' (ADotT (Pattern' a)))) -> Pattern' a -> m (Pattern' a) Source #
ExprLike a => ExprLike (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Pattern' a) Source # foldExpr :: FoldExprFn m (Pattern' a) Source # traverseExpr :: TraverseExprFn m (Pattern' a) Source # mapExpr :: (Expr -> Expr) -> Pattern' a -> Pattern' a Source #
IsWithP (Pattern' e) Source #	Check for with-pattern.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods isWithP :: Pattern' e -> Maybe (Pattern' e) Source #
NamesIn (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn' :: Monoid m => (QName -> m) -> Pattern' a -> m Source #
HasRange (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Pattern' e -> Range Source #
KillRange e => KillRange (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Pattern' e) Source #
SetRange (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> Pattern' a -> Pattern' a Source #
ToConcrete (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe Pattern) Source # Methods toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source # bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Pattern' Expr) Source # Methods toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr)) Source #
ExpandPatternSynonyms (Pattern' e) Source #
Instance details Defined in Agda.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: Pattern' e -> TCM (Pattern' e) Source #
EmbPrj a => EmbPrj (Pattern' a) Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: Pattern' a -> S Int32 Source # icod_ :: Pattern' a -> S Int32 Source # value :: Int32 -> R (Pattern' a) Source #
Data e => Data (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' e -> c (Pattern' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' e) # toConstr :: Pattern' e -> Constr # dataTypeOf :: Pattern' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Pattern' e)) # gmapT :: (forall b. Data b => b -> b) -> Pattern' e -> Pattern' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' e -> r # gmapQ :: (forall d. Data d => d -> u) -> Pattern' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' e -> m (Pattern' e) #
Generic (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Pattern' e) :: Type -> Type # Methods from :: Pattern' e -> Rep (Pattern' e) x # to :: Rep (Pattern' e) x -> Pattern' e #
Show e => Show (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pattern' e -> ShowS # show :: Pattern' e -> String # showList :: [Pattern' e] -> ShowS #
NFData e => NFData (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pattern' e -> () #
Eq e => Eq (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pattern' e -> Pattern' e -> Bool # (/=) :: Pattern' e -> Pattern' e -> Bool #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #
type ConOfAbs Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern
type ADotT (Pattern' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern type ADotT (Pattern' a) = a
type ConOfAbs (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfCon (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr
type Rep (Pattern' e) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (Pattern' e) = D1 ('MetaData "Pattern'" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (((C1 ('MetaCons "VarP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)) :+: (C1 ('MetaCons "ConP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConPatInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "ProjP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName))))) :+: ((C1 ('MetaCons "DefP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))) :+: C1 ('MetaCons "WildP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo))) :+: (C1 ('MetaCons "AsP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e)))) :+: C1 ('MetaCons "DotP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e))))) :+: ((C1 ('MetaCons "AbsurdP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo)) :+: (C1 ('MetaCons "LitP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "PatternSynP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NAPs e)))))) :+: ((C1 ('MetaCons "RecP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FieldAssignment' (Pattern' e)])) :+: C1 ('MetaCons "EqualP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(e, e)]))) :+: (C1 ('MetaCons "WithP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))) :+: C1 ('MetaCons "AnnP" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 e) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' e))))))))
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type LHSCore = LHSCore' Expr Source #

data LHSCore' e Source #

The lhs in projection-application and with-pattern view. Parameterised over the type e of dot patterns.

Constructors

LHSHead	The head applied to ordinary patterns.
Fields lhsDefName :: QName Head `f`. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSProj	Projection.
Fields lhsDestructor :: AmbiguousQName Record projection identifier. lhsFocus :: NamedArg (LHSCore' e) Main argument of projection. lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.
LHSWith	With patterns.
Fields lhsHead :: LHSCore' e E.g. the `LHSHead`. lhsWithPatterns :: [Arg (Pattern' e)] Applied to with patterns `\| p1 \| ... \| pn`. These patterns are not prefixed with `WithP`! lhsPats :: [NamedArg (Pattern' e)] Applied to patterns `ps`.

Instances

Instances details

ToConcrete LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LHSCore Source # Methods toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source # bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b Source #
Foldable LHSCore' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => LHSCore' m -> m # foldMap :: Monoid m => (a -> m) -> LHSCore' a -> m # foldMap' :: Monoid m => (a -> m) -> LHSCore' a -> m # foldr :: (a -> b -> b) -> b -> LHSCore' a -> b # foldr' :: (a -> b -> b) -> b -> LHSCore' a -> b # foldl :: (b -> a -> b) -> b -> LHSCore' a -> b # foldl' :: (b -> a -> b) -> b -> LHSCore' a -> b # foldr1 :: (a -> a -> a) -> LHSCore' a -> a # foldl1 :: (a -> a -> a) -> LHSCore' a -> a # toList :: LHSCore' a -> [a] # null :: LHSCore' a -> Bool # length :: LHSCore' a -> Int # elem :: Eq a => a -> LHSCore' a -> Bool # maximum :: Ord a => LHSCore' a -> a # minimum :: Ord a => LHSCore' a -> a # sum :: Num a => LHSCore' a -> a # product :: Num a => LHSCore' a -> a #
Traversable LHSCore' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> LHSCore' a -> f (LHSCore' b) # sequenceA :: Applicative f => LHSCore' (f a) -> f (LHSCore' a) # mapM :: Monad m => (a -> m b) -> LHSCore' a -> m (LHSCore' b) # sequence :: Monad m => LHSCore' (m a) -> m (LHSCore' a) #
Functor LHSCore' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> LHSCore' a -> LHSCore' b # (<$) :: a -> LHSCore' b -> LHSCore' a #
ExprLike a => ExprLike (LHSCore' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (LHSCore' a) Source # foldExpr :: FoldExprFn m (LHSCore' a) Source # traverseExpr :: TraverseExprFn m (LHSCore' a) Source # mapExpr :: (Expr -> Expr) -> LHSCore' a -> LHSCore' a Source #
HasRange (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHSCore' e -> Range Source #
KillRange e => KillRange (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (LHSCore' e) Source #
ToAbstract (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (LHSCore' Expr) Source # Methods toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr)) Source #
Data e => Data (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHSCore' e -> c (LHSCore' e) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LHSCore' e) # toConstr :: LHSCore' e -> Constr # dataTypeOf :: LHSCore' e -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LHSCore' e)) # dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (LHSCore' e)) # gmapT :: (forall b. Data b => b -> b) -> LHSCore' e -> LHSCore' e # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHSCore' e -> r # gmapQ :: (forall d. Data d => d -> u) -> LHSCore' e -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHSCore' e -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHSCore' e -> m (LHSCore' e) #
Generic (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (LHSCore' e) :: Type -> Type # Methods from :: LHSCore' e -> Rep (LHSCore' e) x # to :: Rep (LHSCore' e) x -> LHSCore' e #
Show e => Show (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHSCore' e -> ShowS # show :: LHSCore' e -> String # showList :: [LHSCore' e] -> ShowS #
NFData e => NFData (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LHSCore' e -> () #
Eq e => Eq (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHSCore' e -> LHSCore' e -> Bool # (/=) :: LHSCore' e -> LHSCore' e -> Bool #
type ConOfAbs LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern
type AbsOfCon (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr
type Rep (LHSCore' e) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (LHSCore' e) = D1 ('MetaData "LHSCore'" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "LHSHead" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])) :+: (C1 ('MetaCons "LHSProj" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsDestructor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName) :: (S1 ('MetaSel ('Just "lhsFocus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg (LHSCore' e))) :: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)]))) :+: C1 ('MetaCons "LHSWith" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsHead") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LHSCore' e)) :: (S1 ('MetaSel ('Just "lhsWithPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg (Pattern' e)]) :*: S1 ('MetaSel ('Just "lhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg (Pattern' e)])))))

data LHS Source #

The lhs of a clause in focused (projection-application) view (outside-in). Projection patters are represented as LHSProjs.

Constructors

LHS
Fields lhsInfo :: LHSInfo Range. lhsCore :: LHSCore Copatterns.

Instances

Instances details

DeclaredNames Clause Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source #
ExprLike LHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LHS Source # foldExpr :: FoldExprFn m LHS Source # traverseExpr :: TraverseExprFn m LHS Source # mapExpr :: (Expr -> Expr) -> LHS -> LHS Source #
HasRange LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LHS -> Range Source #
KillRange LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LHS Source #
ToConcrete LHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LHS Source # Methods toConcrete :: LHS -> AbsToCon (ConOfAbs LHS) Source # bindToConcrete :: LHS -> (ConOfAbs LHS -> AbsToCon b) -> AbsToCon b Source #
Data LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LHS -> c LHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LHS # toConstr :: LHS -> Constr # dataTypeOf :: LHS -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LHS) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LHS) # gmapT :: (forall b. Data b => b -> b) -> LHS -> LHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LHS -> r # gmapQ :: (forall d. Data d => d -> u) -> LHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LHS -> m LHS #
Generic LHS Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LHS :: Type -> Type # Methods from :: LHS -> Rep LHS x # to :: Rep LHS x -> LHS #
Show LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LHS -> ShowS # show :: LHS -> String # showList :: [LHS] -> ShowS #
NFData LHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LHS -> () #
Eq LHS Source #	Ignore `Range'` when comparing `LHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LHS -> LHS -> Bool # (/=) :: LHS -> LHS -> Bool #
LHSToSpine Clause SpineClause Source #	Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source #	LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
type ConOfAbs LHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHS = LHS
type Rep LHS Source #
Instance details Defined in Agda.Syntax.Abstract type Rep LHS = D1 ('MetaData "LHS" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "LHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "lhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :*: S1 ('MetaSel ('Just "lhsCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSCore)))

data SpineLHS Source #

The lhs of a clause in spine view (inside-out). Projection patterns are contained in spLhsPats, represented as ProjP d.

Constructors

SpineLHS
Fields spLhsInfo :: LHSInfo Range. spLhsDefName :: QName Name of function we are defining. spLhsPats :: [NamedArg Pattern] Elimination by pattern, projections, with-patterns.

Instances

Instances details

ExprLike SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m SpineLHS Source # foldExpr :: FoldExprFn m SpineLHS Source # traverseExpr :: TraverseExprFn m SpineLHS Source # mapExpr :: (Expr -> Expr) -> SpineLHS -> SpineLHS Source #
HasRange SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: SpineLHS -> Range Source #
KillRange SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT SpineLHS Source #
ToConcrete SpineLHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs SpineLHS Source # Methods toConcrete :: SpineLHS -> AbsToCon (ConOfAbs SpineLHS) Source # bindToConcrete :: SpineLHS -> (ConOfAbs SpineLHS -> AbsToCon b) -> AbsToCon b Source #
Data SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpineLHS -> c SpineLHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpineLHS # toConstr :: SpineLHS -> Constr # dataTypeOf :: SpineLHS -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpineLHS) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpineLHS) # gmapT :: (forall b. Data b => b -> b) -> SpineLHS -> SpineLHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpineLHS -> r # gmapQ :: (forall d. Data d => d -> u) -> SpineLHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SpineLHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpineLHS -> m SpineLHS #
Generic SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep SpineLHS :: Type -> Type # Methods from :: SpineLHS -> Rep SpineLHS x # to :: Rep SpineLHS x -> SpineLHS #
Show SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> SpineLHS -> ShowS # show :: SpineLHS -> String # showList :: [SpineLHS] -> ShowS #
NFData SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: SpineLHS -> () #
Eq SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: SpineLHS -> SpineLHS -> Bool # (/=) :: SpineLHS -> SpineLHS -> Bool #
LHSToSpine Clause SpineClause Source #	Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
LHSToSpine LHS SpineLHS Source #	LHS instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: LHS -> SpineLHS Source # spineToLhs :: SpineLHS -> LHS Source #
type ConOfAbs SpineLHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs SpineLHS = LHS
type Rep SpineLHS Source #
Instance details Defined in Agda.Syntax.Abstract type Rep SpineLHS = D1 ('MetaData "SpineLHS" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "SpineLHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "spLhsInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LHSInfo) :: (S1 ('MetaSel ('Just "spLhsDefName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Just "spLhsPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]))))

data RHS Source #

Constructors

RHS
Fields rhsExpr :: Expr rhsConcrete :: Maybe Expr We store the original concrete expression in case we have to reproduce it during interactive case splitting. `Nothing` for internally generated rhss.
AbsurdRHS
WithRHS QName [WithExpr] [Clause]	The `QName` is the name of the with function.
RewriteRHS
Fields rewriteExprs :: [RewriteEqn] The `QName`s are the names of the generated with functions, one for each `Expr`. rewriteStrippedPats :: [ProblemEq] The patterns stripped by with-desugaring. These are only present if this rewrite follows a with. rewriteRHS :: RHS The RHS should not be another `RewriteRHS`. rewriteWhereDecls :: WhereDeclarations The where clauses are attached to the `RewriteRHS` by

Instances

Instances details

DeclaredNames RHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RHS -> m Source #
ExprLike RHS Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m RHS Source # foldExpr :: FoldExprFn m RHS Source # traverseExpr :: TraverseExprFn m RHS Source # mapExpr :: (Expr -> Expr) -> RHS -> RHS Source #
HasRange RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: RHS -> Range Source #
KillRange RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT RHS Source #
ToConcrete RHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs RHS Source # Methods toConcrete :: RHS -> AbsToCon (ConOfAbs RHS) Source # bindToConcrete :: RHS -> (ConOfAbs RHS -> AbsToCon b) -> AbsToCon b Source #
Data RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RHS -> c RHS # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RHS # toConstr :: RHS -> Constr # dataTypeOf :: RHS -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RHS) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RHS) # gmapT :: (forall b. Data b => b -> b) -> RHS -> RHS # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RHS -> r # gmapQ :: (forall d. Data d => d -> u) -> RHS -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> RHS -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> RHS -> m RHS # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RHS -> m RHS #
Generic RHS Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep RHS :: Type -> Type # Methods from :: RHS -> Rep RHS x # to :: Rep RHS x -> RHS #
Show RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> RHS -> ShowS # show :: RHS -> String # showList :: [RHS] -> ShowS #
NFData RHS Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: RHS -> () #
Eq RHS Source #	Ignore `rhsConcrete` when comparing `RHS`s.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: RHS -> RHS -> Bool # (/=) :: RHS -> RHS -> Bool #
type ConOfAbs RHS Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs RHS = (RHS, [RewriteEqn], [WithExpr], [Declaration])
type Rep RHS Source #
Instance details Defined in Agda.Syntax.Abstract type Rep RHS = D1 ('MetaData "RHS" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) ((C1 ('MetaCons "RHS" 'PrefixI 'True) (S1 ('MetaSel ('Just "rhsExpr") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Just "rhsConcrete") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Expr))) :+: C1 ('MetaCons "AbsurdRHS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "WithRHS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [WithExpr]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: C1 ('MetaCons "RewriteRHS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "rewriteExprs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [RewriteEqn]) :: S1 ('MetaSel ('Just "rewriteStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :: (S1 ('MetaSel ('Just "rewriteRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :: S1 ('MetaSel ('Just "rewriteWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations)))))

type WithExpr = WithExpr' Expr Source #

type WithExpr' e = Named BindName (Arg e) Source #

type RewriteEqn = RewriteEqn' QName BindName Pattern Expr Source #

type SpineClause = Clause' SpineLHS Source #

type Clause = Clause' LHS Source #

data WhereDeclarations Source #

Constructors

WhereDecls
Fields whereModule :: Maybe ModuleName whereDecls :: Maybe Declaration The declaration is a `Section`.

Instances

Instances details

DeclaredNames WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => WhereDeclarations -> m Source #
ExprLike WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m WhereDeclarations Source # foldExpr :: FoldExprFn m WhereDeclarations Source # traverseExpr :: TraverseExprFn m WhereDeclarations Source # mapExpr :: (Expr -> Expr) -> WhereDeclarations -> WhereDeclarations Source #
HasRange WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: WhereDeclarations -> Range Source #
KillRange WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT WhereDeclarations Source #
ToConcrete WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs WhereDeclarations Source # Methods toConcrete :: WhereDeclarations -> AbsToCon (ConOfAbs WhereDeclarations) Source # bindToConcrete :: WhereDeclarations -> (ConOfAbs WhereDeclarations -> AbsToCon b) -> AbsToCon b Source #
Null WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods empty :: WhereDeclarations Source # null :: WhereDeclarations -> Bool Source #
Data WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> WhereDeclarations -> c WhereDeclarations # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c WhereDeclarations # toConstr :: WhereDeclarations -> Constr # dataTypeOf :: WhereDeclarations -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c WhereDeclarations) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c WhereDeclarations) # gmapT :: (forall b. Data b => b -> b) -> WhereDeclarations -> WhereDeclarations # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WhereDeclarations -> r # gmapQ :: (forall d. Data d => d -> u) -> WhereDeclarations -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> WhereDeclarations -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WhereDeclarations -> m WhereDeclarations #
Generic WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep WhereDeclarations :: Type -> Type # Methods from :: WhereDeclarations -> Rep WhereDeclarations x # to :: Rep WhereDeclarations x -> WhereDeclarations #
Show WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> WhereDeclarations -> ShowS # show :: WhereDeclarations -> String # showList :: [WhereDeclarations] -> ShowS #
NFData WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: WhereDeclarations -> () #
Eq WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: WhereDeclarations -> WhereDeclarations -> Bool # (/=) :: WhereDeclarations -> WhereDeclarations -> Bool #
type ConOfAbs WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs WhereDeclarations = WhereClause
type Rep WhereDeclarations Source #
Instance details Defined in Agda.Syntax.Abstract type Rep WhereDeclarations = D1 ('MetaData "WhereDeclarations" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "WhereDecls" 'PrefixI 'True) (S1 ('MetaSel ('Just "whereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)) :*: S1 ('MetaSel ('Just "whereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Declaration))))

data Clause' lhs Source #

We could throw away where clauses at this point and translate them to let. It's not obvious how to remember that the let was really a where clause though, so for the time being we keep it here.

Constructors

Clause
Fields clauseLHS :: lhs clauseStrippedPats :: [ProblemEq] Only in with-clauses where we inherit some already checked patterns from the parent. These live in the context of the parent clause left-hand side. clauseRHS :: RHS clauseWhereDecls :: WhereDeclarations clauseCatchall :: Bool

Instances

Instances details

DeclaredNames Clause Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Clause -> m Source #
Foldable Clause' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => Clause' m -> m # foldMap :: Monoid m => (a -> m) -> Clause' a -> m # foldMap' :: Monoid m => (a -> m) -> Clause' a -> m # foldr :: (a -> b -> b) -> b -> Clause' a -> b # foldr' :: (a -> b -> b) -> b -> Clause' a -> b # foldl :: (b -> a -> b) -> b -> Clause' a -> b # foldl' :: (b -> a -> b) -> b -> Clause' a -> b # foldr1 :: (a -> a -> a) -> Clause' a -> a # foldl1 :: (a -> a -> a) -> Clause' a -> a # toList :: Clause' a -> [a] # null :: Clause' a -> Bool # length :: Clause' a -> Int # elem :: Eq a => a -> Clause' a -> Bool # maximum :: Ord a => Clause' a -> a # minimum :: Ord a => Clause' a -> a # sum :: Num a => Clause' a -> a # product :: Num a => Clause' a -> a #
Traversable Clause' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Clause' a -> f (Clause' b) # sequenceA :: Applicative f => Clause' (f a) -> f (Clause' a) # mapM :: Monad m => (a -> m b) -> Clause' a -> m (Clause' b) # sequence :: Monad m => Clause' (m a) -> m (Clause' a) #
Functor Clause' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Clause' a -> Clause' b # (<$) :: a -> Clause' b -> Clause' a #
LHSToSpine Clause SpineClause Source #	Clause instance.
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods lhsToSpine :: Clause -> SpineClause Source # spineToLhs :: SpineClause -> Clause Source #
ExprLike a => ExprLike (Clause' a) Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Clause' a) Source # foldExpr :: FoldExprFn m (Clause' a) Source # traverseExpr :: TraverseExprFn m (Clause' a) Source # mapExpr :: (Expr -> Expr) -> Clause' a -> Clause' a Source #
HasRange a => HasRange (Clause' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Clause' a -> Range Source #
KillRange a => KillRange (Clause' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Clause' a) Source #
(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Clause' a) Source # Methods toConcrete :: Clause' a -> AbsToCon (ConOfAbs (Clause' a)) Source # bindToConcrete :: Clause' a -> (ConOfAbs (Clause' a) -> AbsToCon b) -> AbsToCon b Source #
Data lhs => Data (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Clause' lhs -> c (Clause' lhs) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Clause' lhs) # toConstr :: Clause' lhs -> Constr # dataTypeOf :: Clause' lhs -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Clause' lhs)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Clause' lhs)) # gmapT :: (forall b. Data b => b -> b) -> Clause' lhs -> Clause' lhs # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Clause' lhs -> r # gmapQ :: (forall d. Data d => d -> u) -> Clause' lhs -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Clause' lhs -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Clause' lhs -> m (Clause' lhs) #
Generic (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Clause' lhs) :: Type -> Type # Methods from :: Clause' lhs -> Rep (Clause' lhs) x # to :: Rep (Clause' lhs) x -> Clause' lhs #
Show lhs => Show (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Clause' lhs -> ShowS # show :: Clause' lhs -> String # showList :: [Clause' lhs] -> ShowS #
NFData lhs => NFData (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Clause' lhs -> () #
Eq lhs => Eq (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Clause' lhs -> Clause' lhs -> Bool # (/=) :: Clause' lhs -> Clause' lhs -> Bool #
type ConOfAbs (Clause' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Clause' a) = [Declaration]
type Rep (Clause' lhs) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (Clause' lhs) = D1 ('MetaData "Clause'" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) ((S1 ('MetaSel ('Just "clauseLHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 lhs) :: S1 ('MetaSel ('Just "clauseStrippedPats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ProblemEq])) :: (S1 ('MetaSel ('Just "clauseRHS") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RHS) :: (S1 ('MetaSel ('Just "clauseWhereDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhereDeclarations) :: S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data ProblemEq Source #

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Constructors

ProblemEq
Fields problemInPat :: Pattern problemInst :: Term problemType :: Dom Type

Instances

Instances details

KillRange ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ProblemEq Source #
PrettyTCM ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
Subst ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg ProblemEq Source # Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #
Data ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq # toConstr :: ProblemEq -> Constr # dataTypeOf :: ProblemEq -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) # gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq #
Generic ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ProblemEq :: Type -> Type # Methods from :: ProblemEq -> Rep ProblemEq x # to :: Rep ProblemEq x -> ProblemEq #
Show ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ProblemEq -> ShowS # show :: ProblemEq -> String # showList :: [ProblemEq] -> ShowS #
NFData ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ProblemEq -> () #
Eq ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ProblemEq -> ProblemEq -> Bool # (/=) :: ProblemEq -> ProblemEq -> Bool #
type SubstArg ProblemEq Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term
type Rep ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))

data DataDefParams Source #

Constructors

DataDefParams
Fields dataDefGeneralizedParams :: Set Name We don't yet know the position of generalized parameters from the data sig, so we keep these in a set on the side. dataDefParams :: [LamBinding]

Instances

Instances details

ExprLike DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m DataDefParams Source # foldExpr :: FoldExprFn m DataDefParams Source # traverseExpr :: TraverseExprFn m DataDefParams Source # mapExpr :: (Expr -> Expr) -> DataDefParams -> DataDefParams Source #
KillRange DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT DataDefParams Source #
Data DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataDefParams -> c DataDefParams # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataDefParams # toConstr :: DataDefParams -> Constr # dataTypeOf :: DataDefParams -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataDefParams) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataDefParams) # gmapT :: (forall b. Data b => b -> b) -> DataDefParams -> DataDefParams # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataDefParams -> r # gmapQ :: (forall d. Data d => d -> u) -> DataDefParams -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DataDefParams -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataDefParams -> m DataDefParams #
Generic DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep DataDefParams :: Type -> Type # Methods from :: DataDefParams -> Rep DataDefParams x # to :: Rep DataDefParams x -> DataDefParams #
Show DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> DataDefParams -> ShowS # show :: DataDefParams -> String # showList :: [DataDefParams] -> ShowS #
NFData DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: DataDefParams -> () #
Eq DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: DataDefParams -> DataDefParams -> Bool # (/=) :: DataDefParams -> DataDefParams -> Bool #
type Rep DataDefParams Source #
Instance details Defined in Agda.Syntax.Abstract type Rep DataDefParams = D1 ('MetaData "DataDefParams" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "DataDefParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "dataDefGeneralizedParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name)) :*: S1 ('MetaSel ('Just "dataDefParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LamBinding])))

data GeneralizeTelescope Source #

Constructors

GeneralizeTel
Fields generalizeTelVars :: Map QName Name Maps generalize variables to the corresponding bound variable (to be introduced by the generalisation). generalizeTel :: Telescope

Instances

Instances details

ExprLike GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m GeneralizeTelescope Source # foldExpr :: FoldExprFn m GeneralizeTelescope Source # traverseExpr :: TraverseExprFn m GeneralizeTelescope Source # mapExpr :: (Expr -> Expr) -> GeneralizeTelescope -> GeneralizeTelescope Source #
KillRange GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT GeneralizeTelescope Source #
Data GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralizeTelescope -> c GeneralizeTelescope # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizeTelescope # toConstr :: GeneralizeTelescope -> Constr # dataTypeOf :: GeneralizeTelescope -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizeTelescope) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralizeTelescope) # gmapT :: (forall b. Data b => b -> b) -> GeneralizeTelescope -> GeneralizeTelescope # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizeTelescope -> r # gmapQ :: (forall d. Data d => d -> u) -> GeneralizeTelescope -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizeTelescope -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizeTelescope -> m GeneralizeTelescope #
Generic GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep GeneralizeTelescope :: Type -> Type # Methods from :: GeneralizeTelescope -> Rep GeneralizeTelescope x # to :: Rep GeneralizeTelescope x -> GeneralizeTelescope #
Show GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> GeneralizeTelescope -> ShowS # show :: GeneralizeTelescope -> String # showList :: [GeneralizeTelescope] -> ShowS #
NFData GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: GeneralizeTelescope -> () #
Eq GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool # (/=) :: GeneralizeTelescope -> GeneralizeTelescope -> Bool #
type Rep GeneralizeTelescope Source #
Instance details Defined in Agda.Syntax.Abstract type Rep GeneralizeTelescope = D1 ('MetaData "GeneralizeTelescope" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "GeneralizeTel" 'PrefixI 'True) (S1 ('MetaSel ('Just "generalizeTelVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName Name)) :*: S1 ('MetaSel ('Just "generalizeTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope)))

type Telescope = [TypedBinding] Source #

type Telescope1 = List1 TypedBinding Source #

data TypedBinding Source #

A typed binding. Appears in dependent function spaces, typed lambdas, and telescopes. It might be tempting to simplify this to only bind a single name at a time, and translate, say, (x y : A) to (x : A)(y : A) before type-checking. However, this would be slightly problematic:

We would have to typecheck the type A several times.
If A contains a meta variable or hole, it would be duplicated by such a translation.

While 1. is only slightly inefficient, 2. would be an outright bug. Duplicating A could not be done naively, we would have to make sure that the metas of the copy are aliases of the metas of the original.

Constructors

TBind Range TacticAttr (List1 (NamedArg Binder)) Expr	As in telescope `(x y z : A)` or type `(x y z : A) -> B`.
TLet Range (List1 LetBinding)	E.g. `(let x = e)` or `(let open M)`.

Instances

Instances details

ExprLike TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m TypedBinding Source # foldExpr :: FoldExprFn m TypedBinding Source # traverseExpr :: TraverseExprFn m TypedBinding Source # mapExpr :: (Expr -> Expr) -> TypedBinding -> TypedBinding Source #
LensHiding TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source #
HasRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: TypedBinding -> Range Source #
KillRange TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT TypedBinding Source #
ToConcrete TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs TypedBinding Source # Methods toConcrete :: TypedBinding -> AbsToCon (ConOfAbs TypedBinding) Source # bindToConcrete :: TypedBinding -> (ConOfAbs TypedBinding -> AbsToCon b) -> AbsToCon b Source #
PrettyTCM TypedBinding Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => TypedBinding -> m Doc Source #
Data TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedBinding -> c TypedBinding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypedBinding # toConstr :: TypedBinding -> Constr # dataTypeOf :: TypedBinding -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypedBinding) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypedBinding) # gmapT :: (forall b. Data b => b -> b) -> TypedBinding -> TypedBinding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedBinding -> r # gmapQ :: (forall d. Data d => d -> u) -> TypedBinding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedBinding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedBinding -> m TypedBinding #
Generic TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep TypedBinding :: Type -> Type # Methods from :: TypedBinding -> Rep TypedBinding x # to :: Rep TypedBinding x -> TypedBinding #
Show TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS #
NFData TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: TypedBinding -> () #
Eq TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: TypedBinding -> TypedBinding -> Bool # (/=) :: TypedBinding -> TypedBinding -> Bool #
type ConOfAbs TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs TypedBinding = Maybe TypedBinding
type Rep TypedBinding Source #
Instance details Defined in Agda.Syntax.Abstract type Rep TypedBinding = D1 ('MetaData "TypedBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "TBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttr)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 (NamedArg Binder))) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "TLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding))))

data LamBinding Source #

A lambda binding is either domain free or typed.

Constructors

DomainFree TacticAttr (NamedArg Binder)	. `x` or `{x}` or `.x` or `{x = y}` or `x@p` or `(p)`
DomainFull TypedBinding	. `(xs:e)` or `{xs:e}` or `(let Ds)`

Instances

Instances details

ExprLike LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LamBinding Source # foldExpr :: FoldExprFn m LamBinding Source # traverseExpr :: TraverseExprFn m LamBinding Source # mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source #
LensHiding LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source #
HasRange LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LamBinding -> Range Source #
KillRange LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LamBinding Source #
ToConcrete LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LamBinding Source # Methods toConcrete :: LamBinding -> AbsToCon (ConOfAbs LamBinding) Source # bindToConcrete :: LamBinding -> (ConOfAbs LamBinding -> AbsToCon b) -> AbsToCon b Source #
Data LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LamBinding -> c LamBinding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LamBinding # toConstr :: LamBinding -> Constr # dataTypeOf :: LamBinding -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LamBinding) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LamBinding) # gmapT :: (forall b. Data b => b -> b) -> LamBinding -> LamBinding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LamBinding -> r # gmapQ :: (forall d. Data d => d -> u) -> LamBinding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LamBinding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LamBinding -> m LamBinding #
Generic LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LamBinding :: Type -> Type # Methods from :: LamBinding -> Rep LamBinding x # to :: Rep LamBinding x -> LamBinding #
Show LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS #
NFData LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LamBinding -> () #
Eq LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LamBinding -> LamBinding -> Bool # (/=) :: LamBinding -> LamBinding -> Bool #
type ConOfAbs LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LamBinding = Maybe LamBinding
type Rep LamBinding Source #
Instance details Defined in Agda.Syntax.Abstract type Rep LamBinding = D1 ('MetaData "LamBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "DomainFree" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticAttr) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Binder))) :+: C1 ('MetaCons "DomainFull" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypedBinding)))

type Binder = Binder' BindName Source #

data Binder' a Source #

Constructors

Binder
Fields binderPattern :: Maybe Pattern binderName :: a

Instances

Instances details

Foldable Binder' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fold :: Monoid m => Binder' m -> m # foldMap :: Monoid m => (a -> m) -> Binder' a -> m # foldMap' :: Monoid m => (a -> m) -> Binder' a -> m # foldr :: (a -> b -> b) -> b -> Binder' a -> b # foldr' :: (a -> b -> b) -> b -> Binder' a -> b # foldl :: (b -> a -> b) -> b -> Binder' a -> b # foldl' :: (b -> a -> b) -> b -> Binder' a -> b # foldr1 :: (a -> a -> a) -> Binder' a -> a # foldl1 :: (a -> a -> a) -> Binder' a -> a # toList :: Binder' a -> [a] # null :: Binder' a -> Bool # length :: Binder' a -> Int # elem :: Eq a => a -> Binder' a -> Bool # maximum :: Ord a => Binder' a -> a # minimum :: Ord a => Binder' a -> a # sum :: Num a => Binder' a -> a # product :: Num a => Binder' a -> a #
Traversable Binder' Source #
Instance details Defined in Agda.Syntax.Abstract Methods traverse :: Applicative f => (a -> f b) -> Binder' a -> f (Binder' b) # sequenceA :: Applicative f => Binder' (f a) -> f (Binder' a) # mapM :: Monad m => (a -> m b) -> Binder' a -> m (Binder' b) # sequence :: Monad m => Binder' (m a) -> m (Binder' a) #
Functor Binder' Source #
Instance details Defined in Agda.Syntax.Abstract Methods fmap :: (a -> b) -> Binder' a -> Binder' b # (<$) :: a -> Binder' b -> Binder' a #
HasRange a => HasRange (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Binder' a -> Range Source #
KillRange a => KillRange (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT (Binder' a) Source #
ToConcrete a => ToConcrete (Binder' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Binder' a) Source # Methods toConcrete :: Binder' a -> AbsToCon (ConOfAbs (Binder' a)) Source # bindToConcrete :: Binder' a -> (ConOfAbs (Binder' a) -> AbsToCon b) -> AbsToCon b Source #
Data a => Data (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder' a -> c (Binder' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binder' a) # toConstr :: Binder' a -> Constr # dataTypeOf :: Binder' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binder' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Binder' a)) # gmapT :: (forall b. Data b => b -> b) -> Binder' a -> Binder' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Binder' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder' a -> m (Binder' a) #
Generic (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep (Binder' a) :: Type -> Type # Methods from :: Binder' a -> Rep (Binder' a) x # to :: Rep (Binder' a) x -> Binder' a #
Show a => Show (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Binder' a -> ShowS # show :: Binder' a -> String # showList :: [Binder' a] -> ShowS #
NFData a => NFData (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Binder' a -> () #
Eq a => Eq (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Binder' a -> Binder' a -> Bool # (/=) :: Binder' a -> Binder' a -> Bool #
type ConOfAbs (Binder' a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Binder' a) = Binder' (ConOfAbs a)
type Rep (Binder' a) Source #
Instance details Defined in Agda.Syntax.Abstract type Rep (Binder' a) = D1 ('MetaData "Binder'" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "Binder" 'PrefixI 'True) (S1 ('MetaSel ('Just "binderPattern") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Pattern)) :*: S1 ('MetaSel ('Just "binderName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

type TacticAttr = Maybe Expr Source #

type Field = TypeSignature Source #

type Constructor = TypeSignature Source #

type TypeSignature = Declaration Source #

Only Axioms.

data LetBinding Source #

Bindings that are valid in a let.

Constructors

LetBind LetInfo ArgInfo BindName Expr Expr	LetBind info rel name type defn
LetPatBind LetInfo Pattern Expr	Irrefutable pattern binding.
LetApply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective	`LetApply mi newM (oldM args) renamings dir`. The `ImportDirective` is for highlighting purposes.
LetOpen ModuleInfo ModuleName ImportDirective	only for highlighting and abstractToConcrete
LetDeclaredVariable BindName	Only used for highlighting. Refers to the first occurrence of `x` in `let x : A; x = e`. \| LetGeneralize DefInfo ArgInfo Expr

Instances

Instances details

ExprLike LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m LetBinding Source # foldExpr :: FoldExprFn m LetBinding Source # traverseExpr :: TraverseExprFn m LetBinding Source # mapExpr :: (Expr -> Expr) -> LetBinding -> LetBinding Source #
HasRange LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: LetBinding -> Range Source #
KillRange LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT LetBinding Source #
ToConcrete LetBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LetBinding Source # Methods toConcrete :: LetBinding -> AbsToCon (ConOfAbs LetBinding) Source # bindToConcrete :: LetBinding -> (ConOfAbs LetBinding -> AbsToCon b) -> AbsToCon b Source #
Data LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LetBinding -> c LetBinding # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LetBinding # toConstr :: LetBinding -> Constr # dataTypeOf :: LetBinding -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LetBinding) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LetBinding) # gmapT :: (forall b. Data b => b -> b) -> LetBinding -> LetBinding # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LetBinding -> r # gmapQ :: (forall d. Data d => d -> u) -> LetBinding -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LetBinding -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LetBinding -> m LetBinding #
Generic LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep LetBinding :: Type -> Type # Methods from :: LetBinding -> Rep LetBinding x # to :: Rep LetBinding x -> LetBinding #
Show LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> LetBinding -> ShowS # show :: LetBinding -> String # showList :: [LetBinding] -> ShowS #
NFData LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: LetBinding -> () #
Eq LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: LetBinding -> LetBinding -> Bool # (/=) :: LetBinding -> LetBinding -> Bool #
type ConOfAbs LetBinding Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LetBinding = [Declaration]
type Rep LetBinding Source #
Instance details Defined in Agda.Syntax.Abstract type Rep LetBinding = D1 ('MetaData "LetBinding" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) ((C1 ('MetaCons "LetBind" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "LetPatBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LetInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "LetApply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "LetOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "LetDeclaredVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BindName)))))

data Pragma Source #

Constructors

OptionsPragma [String]
BuiltinPragma RString ResolvedName	`ResolvedName` is not `UnknownName`. Name can be ambiguous e.g. for built-in constructors.
BuiltinNoDefPragma RString KindOfName QName	Builtins that do not come with a definition, but declare a name for an Agda concept.
RewritePragma Range [QName]	Range is range of REWRITE keyword.
CompilePragma RString QName String
StaticPragma QName
EtaPragma QName	For coinductive records, use pragma instead of regular `eta-equality` definition (as it is might make Agda loop).
InjectivePragma QName
InlinePragma Bool QName
DisplayPragma QName [NamedArg Pattern] Expr

Instances

Instances details

DeclaredNames Pragma Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Pragma -> m Source #
ExprLike Pragma Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Pragma Source # foldExpr :: FoldExprFn m Pragma Source # traverseExpr :: TraverseExprFn m Pragma Source # mapExpr :: (Expr -> Expr) -> Pragma -> Pragma Source #
Data Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pragma -> c Pragma # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Pragma # toConstr :: Pragma -> Constr # dataTypeOf :: Pragma -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Pragma) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pragma) # gmapT :: (forall b. Data b => b -> b) -> Pragma -> Pragma # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pragma -> r # gmapQ :: (forall d. Data d => d -> u) -> Pragma -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Pragma -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pragma -> m Pragma #
Generic Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Pragma :: Type -> Type # Methods from :: Pragma -> Rep Pragma x # to :: Rep Pragma x -> Pragma #
Show Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Pragma -> ShowS # show :: Pragma -> String # showList :: [Pragma] -> ShowS #
NFData Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Pragma -> () #
Eq Pragma Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Pragma -> Pragma -> Bool # (/=) :: Pragma -> Pragma -> Bool #
type Rep Pragma Source #
Instance details Defined in Agda.Syntax.Abstract type Rep Pragma = D1 ('MetaData "Pragma" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (((C1 ('MetaCons "OptionsPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :+: C1 ('MetaCons "BuiltinPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ResolvedName))) :+: (C1 ('MetaCons "BuiltinNoDefPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "RewritePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])) :+: C1 ('MetaCons "CompilePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RString) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))) :+: ((C1 ('MetaCons "StaticPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "EtaPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))) :+: (C1 ('MetaCons "InjectivePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "InlinePragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "DisplayPragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Pattern]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))

data ModuleApplication Source #

Constructors

SectionApp Telescope ModuleName [NamedArg Expr]	`tel. M args`: applies `M` to `args` and abstracts `tel`.
RecordModuleInstance ModuleName	M {{...}}

Instances

Instances details

ExprLike ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m ModuleApplication Source # foldExpr :: FoldExprFn m ModuleApplication Source # traverseExpr :: TraverseExprFn m ModuleApplication Source # mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source #
KillRange ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ModuleApplication Source #
ToConcrete ModuleApplication Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs ModuleApplication Source # Methods toConcrete :: ModuleApplication -> AbsToCon (ConOfAbs ModuleApplication) Source # bindToConcrete :: ModuleApplication -> (ConOfAbs ModuleApplication -> AbsToCon b) -> AbsToCon b Source #
Data ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModuleApplication -> c ModuleApplication # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModuleApplication # toConstr :: ModuleApplication -> Constr # dataTypeOf :: ModuleApplication -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ModuleApplication) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleApplication) # gmapT :: (forall b. Data b => b -> b) -> ModuleApplication -> ModuleApplication # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModuleApplication -> r # gmapQ :: (forall d. Data d => d -> u) -> ModuleApplication -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ModuleApplication -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModuleApplication -> m ModuleApplication #
Generic ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ModuleApplication :: Type -> Type # Methods from :: ModuleApplication -> Rep ModuleApplication x # to :: Rep ModuleApplication x -> ModuleApplication #
Show ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ModuleApplication -> ShowS # show :: ModuleApplication -> String # showList :: [ModuleApplication] -> ShowS #
NFData ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ModuleApplication -> () #
Eq ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ModuleApplication -> ModuleApplication -> Bool # (/=) :: ModuleApplication -> ModuleApplication -> Bool #
type ConOfAbs ModuleApplication Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs ModuleApplication = ModuleApplication
type Rep ModuleApplication Source #
Instance details Defined in Agda.Syntax.Abstract type Rep ModuleApplication = D1 ('MetaData "ModuleApplication" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "SectionApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NamedArg Expr]))) :+: C1 ('MetaCons "RecordModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)))

type ImportedName = ImportedName' QName ModuleName Source #

type Renaming = Renaming' QName ModuleName Source #

type ImportDirective = ImportDirective' QName ModuleName Source #

type DefInfo = DefInfo' Expr Source #

data Declaration Source #

Constructors

Axiom KindOfName DefInfo ArgInfo (Maybe [Occurrence]) QName Expr	Type signature (can be irrelevant, but not hidden). The fourth argument contains an optional assignment of polarities to arguments.
Generalize (Set QName) DefInfo ArgInfo QName Expr	First argument is set of generalizable variables used in the type.
Field DefInfo QName (Arg Expr)	record field
Primitive DefInfo QName (Arg Expr)	primitive function
Mutual MutualInfo [Declaration]	a bunch of mutually recursive definitions
Section Range ModuleName GeneralizeTelescope [Declaration]
Apply ModuleInfo ModuleName ModuleApplication ScopeCopyInfo ImportDirective	The `ImportDirective` is for highlighting purposes.
Import ModuleInfo ModuleName ImportDirective	The `ImportDirective` is for highlighting purposes.
Pragma Range Pragma
Open ModuleInfo ModuleName ImportDirective	only retained for highlighting purposes
FunDef DefInfo QName Delayed [Clause]	sequence of function clauses
DataSig DefInfo QName GeneralizeTelescope Expr	lone data signature
DataDef DefInfo QName UniverseCheck DataDefParams [Constructor]
RecSig DefInfo QName GeneralizeTelescope Expr	lone record signature
RecDef DefInfo QName UniverseCheck RecordDirectives DataDefParams Expr [Declaration]	The `Expr` gives the constructor type telescope, `(x1 : A1)..(xn : An) -> Prop`, and the optional name is the constructor's name. The optional `Range'` is for the `pattern` attribute.
PatternSynDef QName [Arg BindName] (Pattern' Void)	Only for highlighting purposes
UnquoteDecl MutualInfo [DefInfo] [QName] Expr
UnquoteDef [DefInfo] [QName] Expr
ScopedDecl ScopeInfo [Declaration]	scope annotation

Instances

Instances details

AnyAbstract Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods anyAbstract :: Declaration -> Bool Source #
DeclaredNames Declaration Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Declaration -> m Source #
ExprLike Declaration Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Declaration Source # foldExpr :: FoldExprFn m Declaration Source # traverseExpr :: TraverseExprFn m Declaration Source # mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source #
HasRange Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Declaration -> Range Source #
KillRange Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Declaration Source #
ToConcrete Declaration Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Declaration Source # Methods toConcrete :: Declaration -> AbsToCon (ConOfAbs Declaration) Source # bindToConcrete :: Declaration -> (ConOfAbs Declaration -> AbsToCon b) -> AbsToCon b Source #
ShowHead Declaration Source #
Instance details Defined in Agda.TypeChecking.Rules.Decl Methods showHead :: Declaration -> String Source #
Data Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Declaration -> c Declaration # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Declaration # toConstr :: Declaration -> Constr # dataTypeOf :: Declaration -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Declaration) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Declaration) # gmapT :: (forall b. Data b => b -> b) -> Declaration -> Declaration # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Declaration -> r # gmapQ :: (forall d. Data d => d -> u) -> Declaration -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Declaration -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Declaration -> m Declaration #
Generic Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Declaration :: Type -> Type # Methods from :: Declaration -> Rep Declaration x # to :: Rep Declaration x -> Declaration #
Show Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS #
NFData Declaration Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Declaration -> () #
Eq Declaration Source #	Does not compare `ScopeInfo` fields.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Declaration -> Declaration -> Bool # (/=) :: Declaration -> Declaration -> Bool #
ToConcrete (Constr Constructor) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Constr Constructor) Source # Methods toConcrete :: Constr Constructor -> AbsToCon (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: Constr Constructor -> (ConOfAbs (Constr Constructor) -> AbsToCon b) -> AbsToCon b Source #
type ConOfAbs Declaration Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Declaration = [Declaration]
type Rep Declaration Source #
Instance details Defined in Agda.Syntax.Abstract type Rep Declaration = D1 ('MetaData "Declaration" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) ((((C1 ('MetaCons "Axiom" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KindOfName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [Occurrence])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: C1 ('MetaCons "Generalize" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)))))) :+: ((C1 ('MetaCons "Mutual" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])) :+: C1 ('MetaCons "Section" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: (C1 ('MetaCons "Apply" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleApplication) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeCopyInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective)))) :+: (C1 ('MetaCons "Import" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "Pragma" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pragma)))))) :+: (((C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModuleName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ImportDirective))) :+: C1 ('MetaCons "FunDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Delayed) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause])))) :+: (C1 ('MetaCons "DataSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "DataDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constructor])))) :+: C1 ('MetaCons "RecSig" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralizeTelescope) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))) :+: ((C1 ('MetaCons "RecDef" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UniverseCheck))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordDirectives) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataDefParams)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))) :+: C1 ('MetaCons "PatternSynDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg BindName]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' Void))))) :+: (C1 ('MetaCons "UnquoteDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MutualInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: (C1 ('MetaCons "UnquoteDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DefInfo]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "ScopedDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Declaration])))))))
type ConOfAbs (Constr Constructor) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Constr Constructor) = Declaration

type RecordDirectives = RecordDirectives' QName Source #

data ScopeCopyInfo Source #

Constructors

ScopeCopyInfo
Fields renModules :: Ren ModuleName renNames :: Ren QName

Instances

Instances details

KillRange ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT ScopeCopyInfo Source #
Pretty ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods pretty :: ScopeCopyInfo -> Doc Source # prettyPrec :: Int -> ScopeCopyInfo -> Doc Source # prettyList :: [ScopeCopyInfo] -> Doc Source #
Data ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ScopeCopyInfo -> c ScopeCopyInfo # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ScopeCopyInfo # toConstr :: ScopeCopyInfo -> Constr # dataTypeOf :: ScopeCopyInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ScopeCopyInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ScopeCopyInfo) # gmapT :: (forall b. Data b => b -> b) -> ScopeCopyInfo -> ScopeCopyInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopeCopyInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> ScopeCopyInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopeCopyInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopeCopyInfo -> m ScopeCopyInfo #
Generic ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ScopeCopyInfo :: Type -> Type # Methods from :: ScopeCopyInfo -> Rep ScopeCopyInfo x # to :: Rep ScopeCopyInfo x -> ScopeCopyInfo #
Show ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> ScopeCopyInfo -> ShowS # show :: ScopeCopyInfo -> String # showList :: [ScopeCopyInfo] -> ShowS #
NFData ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: ScopeCopyInfo -> () #
Eq ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool # (/=) :: ScopeCopyInfo -> ScopeCopyInfo -> Bool #
type Rep ScopeCopyInfo Source #
Instance details Defined in Agda.Syntax.Abstract type Rep ScopeCopyInfo = D1 ('MetaData "ScopeCopyInfo" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "ScopeCopyInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "renModules") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren ModuleName)) :*: S1 ('MetaSel ('Just "renNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Ren QName))))

type Ren a = Map a (List1 a) Source #

Renaming (generic).

type RecordAssigns = [RecordAssign] Source #

type RecordAssign = Either Assign ModuleName Source #

type Assigns = [Assign] Source #

type Assign = FieldAssignment' Expr Source #

Record field assignment f = e.

data Expr Source #

Expressions after scope checking (operators parsed, names resolved).

Constructors

Var Name	Bound variable.
Def' QName Suffix	Constant: axiom, function, data or record type, with a possible suffix.
Proj ProjOrigin AmbiguousQName	Projection (overloaded).
Con AmbiguousQName	Constructor (overloaded).
PatternSyn AmbiguousQName	Pattern synonym.
Macro QName	Macro.
Lit ExprInfo Literal	Literal.
QuestionMark MetaInfo InteractionId	Meta variable for interaction. The `InteractionId` is usually identical with the `metaNumber` of `MetaInfo`. However, if you want to print an interaction meta as just `?` instead of `?n`, you should set the `metaNumber` to `Nothing` while keeping the `InteractionId`.
Underscore MetaInfo	Meta variable for hidden argument (must be inferred locally).
Dot ExprInfo Expr	`.e`, for postfix projection.
App AppInfo Expr (NamedArg Expr)	Ordinary (binary) application.
WithApp ExprInfo Expr [Expr]	With application.
Lam ExprInfo LamBinding Expr	`λ bs → e`.
AbsurdLam ExprInfo Hiding	`λ()` or `λ{}`.
ExtendedLam ExprInfo DefInfo Erased QName (List1 Clause)
Pi ExprInfo Telescope1 Expr	Dependent function space `Γ → A`.
Generalized (Set QName) Expr	Like a Pi, but the ordering is not known
Fun ExprInfo (Arg Expr) Expr	Non-dependent function space.
Let ExprInfo (List1 LetBinding) Expr	`let bs in e`.
ETel Telescope	Only used when printing telescopes.
Rec ExprInfo RecordAssigns	Record construction.
RecUpdate ExprInfo Expr Assigns	Record update.
ScopedExpr ScopeInfo Expr	Scope annotation.
Quote ExprInfo	Quote an identifier `QName`.
QuoteTerm ExprInfo	Quote a term.
Unquote ExprInfo	The splicing construct: unquote ...
DontCare Expr	For printing `DontCare` from `Syntax.Internal`.

Instances

Instances details

SubstExpr Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> Expr -> Expr Source #
IsProjP Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods isProjP :: Expr -> Maybe (ProjOrigin, AmbiguousQName) Source #
MapNamedArgPattern NAP Source #
Instance details Defined in Agda.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> NAP -> NAP Source #
ExprLike Expr Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m Expr Source # foldExpr :: FoldExprFn m Expr Source # traverseExpr :: TraverseExprFn m Expr Source # mapExpr :: (Expr -> Expr) -> Expr -> Expr Source #
Underscore Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods underscore :: Expr Source # isUnderscore :: Expr -> Bool Source #
HasRange Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: Expr -> Range Source #
KillRange Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT Expr Source #
ToConcrete Expr Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Expr Source # Methods toConcrete :: Expr -> AbsToCon (ConOfAbs Expr) Source # bindToConcrete :: Expr -> (ConOfAbs Expr -> AbsToCon b) -> AbsToCon b Source #
ToConcrete LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs LHSCore Source # Methods toConcrete :: LHSCore -> AbsToCon (ConOfAbs LHSCore) Source # bindToConcrete :: LHSCore -> (ConOfAbs LHSCore -> AbsToCon b) -> AbsToCon b Source #
ToConcrete Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs Pattern Source # Methods toConcrete :: Pattern -> AbsToCon (ConOfAbs Pattern) Source # bindToConcrete :: Pattern -> (ConOfAbs Pattern -> AbsToCon b) -> AbsToCon b Source #
Reify Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Expr Source # Methods reify :: MonadReify m => Expr -> m (ReifiesTo Expr) Source # reifyWhen :: MonadReify m => Bool -> Expr -> m (ReifiesTo Expr) Source #
PrettyTCM Expr Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Expr -> m Doc Source #
IsFlexiblePattern Pattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool Source #
Data Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Expr -> c Expr # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Expr # toConstr :: Expr -> Constr # dataTypeOf :: Expr -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Expr) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr) # gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r # gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Expr -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Expr -> m Expr #
Generic Expr Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep Expr :: Type -> Type # Methods from :: Expr -> Rep Expr x # to :: Rep Expr x -> Expr #
Show Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
NFData Expr Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: Expr -> () #
Eq Expr Source #	Does not compare `ScopeInfo` fields. Does not distinguish between prefix and postfix projections.
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
ToConcrete (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe Pattern) Source # Methods toConcrete :: Maybe Pattern -> AbsToCon (ConOfAbs (Maybe Pattern)) Source # bindToConcrete :: Maybe Pattern -> (ConOfAbs (Maybe Pattern) -> AbsToCon b) -> AbsToCon b Source #
PrettyTCM (Arg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Arg Expr -> m Doc Source #
PrettyTCM (NamedArg Expr) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedArg Expr -> m Doc Source #
ToAbstract (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elim) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #
ToAbstract (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elims) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #
type ConOfAbs Expr Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Expr = Expr
type ConOfAbs LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs LHSCore = Pattern
type ConOfAbs Pattern Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs Pattern = Pattern
type ReifiesTo Expr Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Expr = Expr
type Rep Expr Source #
Instance details Defined in Agda.Syntax.Abstract type Rep Expr = D1 ('MetaData "Expr" "Agda.Syntax.Abstract" "Agda-2.6.2.1.20220327-inplace" 'False) ((((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "Def'" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Suffix)) :+: C1 ('MetaCons "Proj" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProjOrigin) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)))) :+: (C1 ('MetaCons "Con" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: (C1 ('MetaCons "PatternSyn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AmbiguousQName)) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "Lit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: (C1 ('MetaCons "QuestionMark" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InteractionId)) :+: C1 ('MetaCons "Underscore" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaInfo)))) :+: ((C1 ('MetaCons "Dot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AppInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NamedArg Expr))))) :+: (C1 ('MetaCons "WithApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Expr]))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LamBinding) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))))) :+: (((C1 ('MetaCons "AbsurdLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Hiding)) :+: (C1 ('MetaCons "ExtendedLam" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefInfo)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 Clause))))) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope1) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))))) :+: ((C1 ('MetaCons "Generalized" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set QName)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "Fun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Expr)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: (C1 ('MetaCons "Let" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (List1 LetBinding)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr))) :+: C1 ('MetaCons "ETel" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope))))) :+: ((C1 ('MetaCons "Rec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RecordAssigns)) :+: (C1 ('MetaCons "RecUpdate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assigns))) :+: C1 ('MetaCons "ScopedExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ScopeInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))) :+: ((C1 ('MetaCons "Quote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "QuoteTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo))) :+: (C1 ('MetaCons "Unquote" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExprInfo)) :+: C1 ('MetaCons "DontCare" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)))))))
type ConOfAbs (Maybe Pattern) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe Pattern) = Maybe Pattern
type AbsOfRef (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr
type AbsOfRef (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

type Args = [NamedArg Expr] Source #

newtype BindName Source #

A name in a binding position: we also compare the nameConcrete when comparing the binders for equality.

With --caching on we compare abstract syntax to determine if we can reuse previous typechecking results: during that comparison two names can have the same nameId but be semantically different, e.g. in {_ : A} -> .. vs. {r : A} -> ...

Constructors

BindName
Fields unBind :: Name

Instances

Instances details

ExprLike BindName Source #
Instance details Defined in Agda.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m BindName Source # foldExpr :: FoldExprFn m BindName Source # traverseExpr :: TraverseExprFn m BindName Source # mapExpr :: (Expr -> Expr) -> BindName -> BindName Source #
HasRange BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods getRange :: BindName -> Range Source #
KillRange BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods killRange :: KillRangeT BindName Source #
SetRange BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods setRange :: Range -> BindName -> BindName Source #
ToConcrete BindName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs BindName Source # Methods toConcrete :: BindName -> AbsToCon (ConOfAbs BindName) Source # bindToConcrete :: BindName -> (ConOfAbs BindName -> AbsToCon b) -> AbsToCon b Source #
EmbPrj BindName Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Abstract Methods icode :: BindName -> S Int32 Source # icod_ :: BindName -> S Int32 Source # value :: Int32 -> R BindName Source #
Data BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BindName -> c BindName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BindName # toConstr :: BindName -> Constr # dataTypeOf :: BindName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BindName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BindName) # gmapT :: (forall b. Data b => b -> b) -> BindName -> BindName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BindName -> r # gmapQ :: (forall d. Data d => d -> u) -> BindName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BindName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BindName -> m BindName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BindName -> m BindName #
Show BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods showsPrec :: Int -> BindName -> ShowS # show :: BindName -> String # showList :: [BindName] -> ShowS #
NFData BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods rnf :: BindName -> () #
Eq BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods (==) :: BindName -> BindName -> Bool # (/=) :: BindName -> BindName -> Bool #
Ord BindName Source #
Instance details Defined in Agda.Syntax.Abstract Methods compare :: BindName -> BindName -> Ordering # (<) :: BindName -> BindName -> Bool # (<=) :: BindName -> BindName -> Bool # (>) :: BindName -> BindName -> Bool # (>=) :: BindName -> BindName -> Bool # max :: BindName -> BindName -> BindName # min :: BindName -> BindName -> BindName #
ToConcrete (Maybe BindName) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (Maybe BindName) Source # Methods toConcrete :: Maybe BindName -> AbsToCon (ConOfAbs (Maybe BindName)) Source # bindToConcrete :: Maybe BindName -> (ConOfAbs (Maybe BindName) -> AbsToCon b) -> AbsToCon b Source #
(ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Associated Types type ConOfAbs (RewriteEqn' qn BindName p a) Source # Methods toConcrete :: RewriteEqn' qn BindName p a -> AbsToCon (ConOfAbs (RewriteEqn' qn BindName p a)) Source # bindToConcrete :: RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> AbsToCon b) -> AbsToCon b Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #
type ConOfAbs BindName Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs BindName = BoundName
type ConOfAbs (Maybe BindName) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (Maybe BindName) = Maybe Name
type ConOfAbs (RewriteEqn' qn BindName p a) Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete type ConOfAbs (RewriteEqn' qn BindName p a) = RewriteEqn' () Name (ConOfAbs p) (ConOfAbs a)
type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn