Agda-2.6.0: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Base

Contents

Synopsis

Type checking state

data TCState Source #

Constructors

TCSt 

Fields

Instances
Show TCState Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensPersistentVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPragmaOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

class Monad m => ReadTCState m where Source #

Methods

getTCState :: m TCState Source #

withTCState :: (TCState -> TCState) -> m a -> m a Source #

Instances
ReadTCState ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

ReadTCState m => ReadTCState (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState m => ReadTCState (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => ReadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState m => ReadTCState (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

ReadTCState m => ReadTCState (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ExceptT err m TCState Source #

withTCState :: (TCState -> TCState) -> ExceptT err m a -> ExceptT err m a Source #

ReadTCState m => ReadTCState (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: StateT s m TCState Source #

withTCState :: (TCState -> TCState) -> StateT s m a -> StateT s m a Source #

(Monoid w, ReadTCState m) => ReadTCState (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState m => ReadTCState (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data PreScopeState Source #

Constructors

PreScopeState 

Fields

data PostScopeState Source #

Constructors

PostScopeState 

Fields

data MutualBlock Source #

A mutual block of names in the signature.

Constructors

MutualBlock 

Fields

data PersistentTCState Source #

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt 

Fields

Instances
LensPersistentVerbosity PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.

type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

Like CachedTypeCheckLog, but storing the log for an ongoing type checking of a module. Stored in reverse order (last performed action first).

data TypeCheckAction Source #

A complete log for a module will look like this:

  • Pragmas
  • EnterSection, entering the main module.
  • 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested modules
  • LeaveSection, leaving the main module.

initPersistentState :: PersistentTCState Source #

Empty persistent state.

initPreScopeState :: PreScopeState Source #

Empty state of type checker.

st-prefixed lenses

Fresh things

newtype ProblemId Source #

Constructors

ProblemId Nat 
Instances
Enum ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Integral ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId #

toConstr :: ProblemId -> Constr #

dataTypeOf :: ProblemId -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) #

gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r #

gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId #

Num ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Real ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

newtype CheckpointId Source #

Constructors

CheckpointId Int 
Instances
Enum CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Integral CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CheckpointId -> c CheckpointId #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CheckpointId #

toConstr :: CheckpointId -> Constr #

dataTypeOf :: CheckpointId -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CheckpointId) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CheckpointId) #

gmapT :: (forall b. Data b => b -> b) -> CheckpointId -> CheckpointId #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r #

gmapQ :: (forall d. Data d => d -> u) -> CheckpointId -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CheckpointId -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId #

Num CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Real CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

class FreshName a where Source #

Create a fresh name from a.

Methods

freshName_ :: MonadTCState m => a -> m Name Source #

Instances
FreshName () Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadTCState m => () -> m Name Source #

FreshName String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Managing file names

type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #

Maps top-level module names to the corresponding source file names.

type SourceToModule = Map AbsolutePath TopLevelModuleName Source #

Maps source file names to the corresponding top-level module names.

sourceToModule :: TCM SourceToModule Source #

Creates a SourceToModule map based on stModuleToSource.

O(n log n).

For a single reverse lookup in stModuleToSource, rather use lookupModuleFromSourse.

Interface

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

data Interface Source #

Constructors

Interface 

Fields

iFullHash :: Interface -> Hash Source #

Combines the source hash and the (full) hashes of the imported modules.

Closure

data Closure a Source #

Instances
Functor Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Closure a -> Closure b #

(<$) :: a -> Closure b -> Closure a #

Foldable Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Closure m -> m #

foldMap :: Monoid m => (a -> m) -> Closure a -> m #

foldr :: (a -> b -> b) -> b -> Closure a -> b #

foldr' :: (a -> b -> b) -> b -> Closure a -> b #

foldl :: (b -> a -> b) -> b -> Closure a -> b #

foldl' :: (b -> a -> b) -> b -> Closure a -> b #

foldr1 :: (a -> a -> a) -> Closure a -> a #

foldl1 :: (a -> a -> a) -> Closure a -> a #

toList :: Closure a -> [a] #

null :: Closure a -> Bool #

length :: Closure a -> Int #

elem :: Eq a => a -> Closure a -> Bool #

maximum :: Ord a => Closure a -> a #

minimum :: Ord a => Closure a -> a #

sum :: Num a => Closure a -> a #

product :: Num a => Closure a -> a #

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Data a => Data (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Closure a -> c (Closure a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Closure a) #

toConstr :: Closure a -> Constr #

dataTypeOf :: Closure a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Closure a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Closure a)) #

gmapT :: (forall b. Data b => b -> b) -> Closure a -> Closure a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Closure a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Closure a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a) #

Show a => Show (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Closure a -> ShowS #

show :: Closure a -> String #

showList :: [Closure a] -> ShowS #

KillRange a => KillRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange a => HasRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range Source #

PrettyTCM a => PrettyTCM (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Closure a -> TCM Doc Source #

MentionsMeta a => MentionsMeta (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull a => InstantiateFull (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise a => Normalise (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify a => Simplify (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce a => Reduce (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate a => Instantiate (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Constraints

data ProblemConstraint Source #

Instances
Data ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemConstraint -> c ProblemConstraint #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemConstraint #

toConstr :: ProblemConstraint -> Constr #

dataTypeOf :: ProblemConstraint -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemConstraint) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemConstraint) #

gmapT :: (forall b. Data b => b -> b) -> ProblemConstraint -> ProblemConstraint #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r #

gmapQ :: (forall d. Data d => d -> u) -> ProblemConstraint -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemConstraint -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint #

Show ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

MentionsMeta ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

data Constraint Source #

Constructors

ValueCmp Comparison Type Term Term 
ValueCmpOnFace Comparison Term Type Term Term 
ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim] 
TypeCmp Comparison Type Type 
TelCmp Type Type Comparison Telescope Telescope

the two types are for the error message only

SortCmp Comparison Sort Sort 
LevelCmp Comparison Level Level 
HasBiggerSort Sort 
HasPTSRule Sort (Abs Sort) 
UnBlock MetaId 
Guarded Constraint ProblemId 
IsEmpty Range Type

The range is the one of the absurd pattern.

CheckSizeLtSat Term

Check that the Term is either not a SIZELT or a non-empty SIZELT.

FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])

the first argument is the instance argument, the second one is the meta on which the constraint may be blocked on and the third one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)

CheckFunDef Delayed DefInfo QName [Clause] 
UnquoteTactic (Maybe MetaId) Term Term Type

First argument is computation and the others are hole and goal type

Instances
Eq Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Data Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constraint -> c Constraint #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constraint #

toConstr :: Constraint -> Constr #

dataTypeOf :: Constraint -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constraint) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint) #

gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r #

gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint #

Show Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

TermLike Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint Source #

foldTerm :: Monoid m => (Term -> m) -> Constraint -> m Source #

PrettyTCM Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

MentionsMeta Constraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify Constraint (OutputConstraint Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

data Comparison Source #

Constructors

CmpEq 
CmpLeq 
Instances
Eq Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comparison -> c Comparison #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comparison #

toConstr :: Comparison -> Constr #

dataTypeOf :: Comparison -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comparison) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comparison) #

gmapT :: (forall b. Data b => b -> b) -> Comparison -> Comparison #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r #

gmapQ :: (forall d. Data d => d -> u) -> Comparison -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Comparison -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison #

Show Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

flipCmp :: CompareDirection -> CompareDirection Source #

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c Source #

Turn a Comparison function into a CompareDirection function.

Property: dirToCmp f (fromCmp cmp) = f cmp

Open things

data Open a Source #

A thing tagged with the context it came from.

Constructors

OpenThing 
Instances
Functor Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Open a -> Open b #

(<$) :: a -> Open b -> Open a #

Foldable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Open m -> m #

foldMap :: Monoid m => (a -> m) -> Open a -> m #

foldr :: (a -> b -> b) -> b -> Open a -> b #

foldr' :: (a -> b -> b) -> b -> Open a -> b #

foldl :: (b -> a -> b) -> b -> Open a -> b #

foldl' :: (b -> a -> b) -> b -> Open a -> b #

foldr1 :: (a -> a -> a) -> Open a -> a #

foldl1 :: (a -> a -> a) -> Open a -> a #

toList :: Open a -> [a] #

null :: Open a -> Bool #

length :: Open a -> Int #

elem :: Eq a => a -> Open a -> Bool #

maximum :: Ord a => Open a -> a #

minimum :: Ord a => Open a -> a #

sum :: Num a => Open a -> a #

product :: Num a => Open a -> a #

Traversable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverse :: Applicative f => (a -> f b) -> Open a -> f (Open b) #

sequenceA :: Applicative f => Open (f a) -> f (Open a) #

mapM :: Monad m => (a -> m b) -> Open a -> m (Open b) #

sequence :: Monad m => Open (m a) -> m (Open a) #

Decoration Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b) Source #

distributeF :: Functor m => Open (m a) -> m (Open a) Source #

Data a => Data (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Open a -> c (Open a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Open a) #

toConstr :: Open a -> Constr #

dataTypeOf :: Open a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Open a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Open a)) #

gmapT :: (forall b. Data b => b -> b) -> Open a -> Open a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Open a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Open a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a) #

Show a => Show (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Open a -> ShowS #

show :: Open a -> String #

showList :: [Open a] -> ShowS #

KillRange a => KillRange (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj a => EmbPrj (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32 Source #

icod_ :: Open a -> S Int32 Source #

value :: Int32 -> R (Open a) Source #

NamesIn a => NamesIn (Open a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Open a -> Set QName Source #

InstantiateFull a => InstantiateFull (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Judgements

data Judgement a Source #

Parametrized since it is used without MetaId when creating a new meta.

Constructors

HasType 

Fields

IsSort 

Fields

Instances
Show a => Show (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM a => PrettyTCM (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Generalizable variables

data DoGeneralize Source #

Instances
Eq DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoGeneralize -> c DoGeneralize #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoGeneralize #

toConstr :: DoGeneralize -> Constr #

dataTypeOf :: DoGeneralize -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoGeneralize) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoGeneralize) #

gmapT :: (forall b. Data b => b -> b) -> DoGeneralize -> DoGeneralize #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r #

gmapQ :: (forall d. Data d => d -> u) -> DoGeneralize -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DoGeneralize -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize #

Ord DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data GeneralizedValue Source #

The value of a generalizable variable. This is created to be a generalizable meta before checking the type to be generalized.

Instances
Data GeneralizedValue Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralizedValue -> c GeneralizedValue #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizedValue #

toConstr :: GeneralizedValue -> Constr #

dataTypeOf :: GeneralizedValue -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizedValue) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralizedValue) #

gmapT :: (forall b. Data b => b -> b) -> GeneralizedValue -> GeneralizedValue #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r #

gmapQ :: (forall d. Data d => d -> u) -> GeneralizedValue -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizedValue -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue #

Show GeneralizedValue Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Meta variables

data MetaVariable Source #

Constructors

MetaVar 

Fields

data Frozen Source #

Frozen meta variable cannot be instantiated by unification. This serves to prevent the completion of a definition by its use outside of the current block. (See issues 118, 288, 399).

Constructors

Frozen

Do not instantiate.

Instantiable 
Instances
Eq Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Frozen -> Frozen -> Bool #

(/=) :: Frozen -> Frozen -> Bool #

Show Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data MetaInstantiation Source #

Constructors

InstV [Arg String] Term

solved by term (abstracted over some free variables)

Open

unsolved

OpenInstance

open, to be instantiated by instance search

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) 

data CheckedTarget Source #

Solving a CheckArgs constraint may or may not check the target type. If it did, it returns a handle to any unsolved constraints.

data TypeCheckingProblem Source #

Constructors

CheckExpr Comparison Expr Type 
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term) 
CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonemptyList QName) Args Type Int Term Type 
CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type

(λ (xs : t₀) → e) : t This is not an instance of CheckExpr as the domain type has already been checked. For example, when checking (λ (x y : Fin _) → e) : (x : Fin n) → ? we want to postpone (λ (y : Fin n) → e) : ? where Fin n is a Type rather than an Expr.

DoQuoteTerm Comparison Term Type

Quote the given term and check type against Term

newtype MetaPriority Source #

Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?

Higher value means higher priority to be instantiated.

Constructors

MetaPriority Int 

data MetaInfo Source #

MetaInfo is cloned from one meta to the next during pruning.

Constructors

MetaInfo 

Fields

Instances
SetRange MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange MetaInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type MetaNameSuggestion = String Source #

Name suggestion for meta variable. Empty string means no suggestion.

data NamedMeta Source #

For printing, we couple a meta with its name suggestion.

Interaction meta variables

data InteractionPoint Source #

Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.

Constructors

InteractionPoint 

Fields

type InteractionPoints = Map InteractionId InteractionPoint Source #

Data structure managing the interaction points.

We never remove interaction points from this map, only set their ipSolved to True. (Issue #2368)

data IPClause Source #

Which clause is an interaction point located in?

Constructors

IPClause 

Fields

IPNoClause

The interaction point is not in the rhs of a clause.

Instances
Eq IPClause Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data IPClause Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IPClause -> c IPClause #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IPClause #

toConstr :: IPClause -> Constr #

dataTypeOf :: IPClause -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IPClause) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IPClause) #

gmapT :: (forall b. Data b => b -> b) -> IPClause -> IPClause #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r #

gmapQ :: (forall d. Data d => d -> u) -> IPClause -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IPClause -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause #

Signature

data Signature Source #

Constructors

Sig 

Fields

Instances
Data Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Signature -> c Signature #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Signature #

toConstr :: Signature -> Constr #

dataTypeOf :: Signature -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Signature) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Signature) #

gmapT :: (forall b. Data b => b -> b) -> Signature -> Signature #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r #

gmapQ :: (forall d. Data d => d -> u) -> Signature -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Signature -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Signature -> m Signature #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature #

Show Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Signature Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull Signature Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

newtype Section Source #

Constructors

Section 
Instances
Eq Section Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: Section -> Section -> Bool #

(/=) :: Section -> Section -> Bool #

Data Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Section -> c Section #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Section #

toConstr :: Section -> Constr #

dataTypeOf :: Section -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Section) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Section) #

gmapT :: (forall b. Data b => b -> b) -> Section -> Section #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r #

gmapQ :: (forall d. Data d => d -> u) -> Section -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Section -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Section -> m Section #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section #

Show Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Sections Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Section Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull Section Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data DisplayForm Source #

A DisplayForm is in essence a rewrite rule q ts --> dt for a defined symbol (could be a constructor as well) q. The right hand side is a DisplayTerm which is used to reify to a more readable Syntax.

The patterns ts are just terms, but var 0 is interpreted as a hole. Each occurrence of var 0 is a new hole (pattern var). For each *occurrence* of var0 the rhs dt has a free variable. These are instantiated when matching a display form against a term q vs succeeds.

Constructors

Display 

Fields

Instances
Data DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayForm -> c DisplayForm #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayForm #

toConstr :: DisplayForm -> Constr #

dataTypeOf :: DisplayForm -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayForm) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayForm) #

gmapT :: (forall b. Data b => b -> b) -> DisplayForm -> DisplayForm #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r #

gmapQ :: (forall d. Data d => d -> u) -> DisplayForm -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayForm -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm #

Show DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn DisplayForm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

InstantiateFull DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data DisplayTerm Source #

A structured presentation of a Term for reification into Syntax.

Constructors

DWithApp DisplayTerm [DisplayTerm] Elims

(f vs | ws) es. The first DisplayTerm is the parent function f with its args vs. The list of DisplayTerms are the with expressions ws. The Elims are additional arguments es (possible in case the with-application is of function type) or projections (if it is of record type).

DCon ConHead ConInfo [Arg DisplayTerm]

c vs.

DDef QName [Elim' DisplayTerm]

d vs.

DDot Term

.v.

DTerm Term

v.

Instances
Data DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayTerm -> c DisplayTerm #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayTerm #

toConstr :: DisplayTerm -> Constr #

dataTypeOf :: DisplayTerm -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayTerm) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayTerm) #

gmapT :: (forall b. Data b => b -> b) -> DisplayTerm -> DisplayTerm #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r #

gmapQ :: (forall d. Data d => d -> u) -> DisplayTerm -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayTerm -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm #

Show DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Apply DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NamesIn DisplayTerm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

InstantiateFull DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SubstWithOrigin DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Subst Term DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify DisplayTerm Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

SubstWithOrigin (Arg DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

defaultDisplayForm :: QName -> [LocalDisplayForm] Source #

By default, we have no display form.

data NLPat Source #

Non-linear (non-constructor) first-order pattern.

Constructors

PVar !Int [Arg Int]

Matches anything (modulo non-linearity) that only contains bound variables that occur in the given arguments.

PWild

Matches anything (e.g. irrelevant terms).

PDef QName PElims

Matches f es

PLam ArgInfo (Abs NLPat)

Matches λ x → t

PPi (Dom NLPType) (Abs NLPType)

Matches (x : A) → B

PBoundVar !Int PElims

Matches x es where x is a lambda-bound variable

PTerm Term

Matches the term modulo β (ideally βη).

Instances
Data NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPat -> c NLPat #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPat #

toConstr :: NLPat -> Constr #

dataTypeOf :: NLPat -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPat) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPat) #

gmapT :: (forall b. Data b => b -> b) -> NLPat -> NLPat #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r #

gmapQ :: (forall d. Data d => d -> u) -> NLPat -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPat -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat #

Show NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPat -> ShowS #

show :: NLPat -> String #

showList :: [NLPat] -> ShowS #

KillRange NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

DeBruijn NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Free NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Methods

freeVars' :: IsVarSet c => NLPat -> FreeM c Source #

EmbPrj NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: NLPat -> TCM Doc Source #

InstantiateFull NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

NLPatVars NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Subst NLPat RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Match () NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM () Source #

Match () NLPat Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Sort -> NLM () Source #

Match Type NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #

PatternFrom () Sort NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPat Source #

PatternFrom Type Term NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PatternFrom (Type, Term) Elims [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Match (Type, Term) [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

data NLPType Source #

Constructors

NLPType 
Instances
Data NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPType -> c NLPType #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPType #

toConstr :: NLPType -> Constr #

dataTypeOf :: NLPType -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPType) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPType) #

gmapT :: (forall b. Data b => b -> b) -> NLPType -> NLPType #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r #

gmapQ :: (forall d. Data d => d -> u) -> NLPType -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPType -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType #

Show NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Methods

freeVars' :: IsVarSet c => NLPType -> FreeM c Source #

EmbPrj NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

NLPatVars NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Subst NLPat NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Match () NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #

PatternFrom () Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #

data RewriteRule Source #

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule 

Fields

Instances
Data RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteRule -> c RewriteRule #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RewriteRule #

toConstr :: RewriteRule -> Constr #

dataTypeOf :: RewriteRule -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RewriteRule) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RewriteRule) #

gmapT :: (forall b. Data b => b -> b) -> RewriteRule -> RewriteRule #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r #

gmapQ :: (forall d. Data d => d -> u) -> RewriteRule -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteRule -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule #

Show RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRuleMap Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract RewriteRule Source #

tel ⊢ (Γ ⊢ lhs ↦ rhs : t) becomes tel, Γ ⊢ lhs ↦ rhs : t) we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.

Instance details

Defined in Agda.TypeChecking.Substitute

Apply RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Subst NLPat RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data Definition Source #

Constructors

Defn 

Fields

Instances
Data Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Definition -> c Definition #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Definition #

toConstr :: Definition -> Constr #

dataTypeOf :: Definition -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Definition) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Definition) #

gmapT :: (forall b. Data b => b -> b) -> Definition -> Definition #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r #

gmapQ :: (forall d. Data d => d -> u) -> Definition -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Definition -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Definition -> m Definition #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition #

Show Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definitions Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj Definition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

NamesIn Definition Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

InstantiateFull Definition Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data NumGeneralizableArgs Source #

Constructors

NoGeneralizableArgs 
SomeGeneralizableArgs Int

When lambda-lifting new args are generalizable if SomeGeneralizableArgs, also when the number is zero.

Instances
Data NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NumGeneralizableArgs -> c NumGeneralizableArgs #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NumGeneralizableArgs #

toConstr :: NumGeneralizableArgs -> Constr #

dataTypeOf :: NumGeneralizableArgs -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NumGeneralizableArgs) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NumGeneralizableArgs) #

gmapT :: (forall b. Data b => b -> b) -> NumGeneralizableArgs -> NumGeneralizableArgs #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NumGeneralizableArgs -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NumGeneralizableArgs -> r #

gmapQ :: (forall d. Data d => d -> u) -> NumGeneralizableArgs -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> NumGeneralizableArgs -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs #

Show NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source #

Create a definition with sensible defaults.

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances
Eq Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Polarity -> c Polarity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Polarity #

toConstr :: Polarity -> Constr #

dataTypeOf :: Polarity -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Polarity) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Polarity) #

gmapT :: (forall b. Data b => b -> b) -> Polarity -> Polarity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Polarity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Polarity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity #

Show Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Abstract [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data IsForced Source #

Information about whether an argument is forced by the type of a function.

Constructors

Forced 
NotForced 
Instances
Eq IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsForced -> c IsForced #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsForced #

toConstr :: IsForced -> Constr #

dataTypeOf :: IsForced -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsForced) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsForced) #

gmapT :: (forall b. Data b => b -> b) -> IsForced -> IsForced #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r #

gmapQ :: (forall d. Data d => d -> u) -> IsForced -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsForced -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced #

Show IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

PrettyTCM IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data CompilerPragma Source #

The backends are responsible for parsing their own pragmas.

Instances
Eq CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompilerPragma -> c CompilerPragma #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompilerPragma #

toConstr :: CompilerPragma -> Constr #

dataTypeOf :: CompilerPragma -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompilerPragma) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompilerPragma) #

gmapT :: (forall b. Data b => b -> b) -> CompilerPragma -> CompilerPragma #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r #

gmapQ :: (forall d. Data d => d -> u) -> CompilerPragma -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CompilerPragma -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma #

Show CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange CompiledRepresentation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

type Face = [(Term, Bool)] Source #

data System Source #

An alternative representation of partial elements in a telescope: Γ ⊢ λ Δ. [φ₁ u₁, ... , φₙ uₙ] : Δ → PartialP (∨_ᵢ φᵢ) T see cubicaltt paper (however we do not store the type T).

Constructors

System 

Fields

  • systemTel :: Telescope

    the telescope Δ, binding vars for the clauses, Γ ⊢ Δ

  • systemClauses :: [(Face, Term)]

    a system [φ₁ u₁, ... , φₙ uₙ] where Γ, Δ ⊢ φᵢ and Γ, Δ, φᵢ ⊢ uᵢ

Instances
Data System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> System -> c System #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c System #

toConstr :: System -> Constr #

dataTypeOf :: System -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c System) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c System) #

gmapT :: (forall b. Data b => b -> b) -> System -> System #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> System -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> System -> r #

gmapQ :: (forall d. Data d => d -> u) -> System -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> System -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> System -> m System #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System #

Show System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj System Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

InstantiateFull System Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract