Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Reduce

Synopsis

Documentation

class Instantiate t Source #

Instantiate something. Results in an open meta variable or a non meta. Doesn't do any reduction, and preserves blocking tags (when blocking meta is uninstantiated).

Instances

Instances details
Instantiate EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Blocker Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate () Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: () -> ReduceM () Source #

Instantiate t => Instantiate (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Arg t -> ReduceM (Arg t) Source #

Instantiate t => Instantiate (Abs t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Abs t -> ReduceM (Abs t) Source #

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

Defined in Agda.TypeChecking.Reduce

Instantiate t => Instantiate (PlusLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate t => Instantiate (Tele t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Tele t -> ReduceM (Tele t) Source #

Instantiate t => Instantiate (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Type' t -> ReduceM (Type' t) Source #

Instantiate t => Instantiate (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Elim' t -> ReduceM (Elim' t) Source #

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

Defined in Agda.TypeChecking.Reduce

Instantiate t => Instantiate (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate t => Instantiate (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Maybe t -> ReduceM (Maybe t) Source #

Instantiate t => Instantiate (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Maybe t -> ReduceM (Maybe t) Source #

Instantiate t => Instantiate [t] Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: [t] -> ReduceM [t] Source #

(Instantiate t, Instantiate e) => Instantiate (Dom' t e) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Dom' t e -> ReduceM (Dom' t e) Source #

Instantiate t => Instantiate (Map k t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Map k t -> ReduceM (Map k t) Source #

(Instantiate a, Instantiate b) => Instantiate (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: (a, b) -> ReduceM (a, b) Source #

(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: (a, b, c) -> ReduceM (a, b, c) Source #

instantiateWhen :: (InstantiateFull a, MonadReduce m) => (MetaId -> ReduceM Bool) -> a -> m a Source #

A variant of instantiateFull that only instantiates those meta-variables that satisfy the predicate.

class InstantiateFull t Source #

instantiateFull' instantiates metas everywhere (and recursively) but does not reduce.

Instances

Instances details
InstantiateFull ModuleName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Name Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull QName Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull PrimitiveId Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Clause Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull ConHead Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Scope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Definition Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Defn Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Instantiation Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Interface Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull LetBinding Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull RemoteMetaVariable Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Section Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull Signature Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull System Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull LHSResult Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

InstantiateFull AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

InstantiateFull Bool Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Bool -> ReduceM Bool Source #

InstantiateFull Char Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Char -> ReduceM Char Source #

InstantiateFull Int Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Int -> ReduceM Int Source #

InstantiateFull t => InstantiateFull (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Arg t -> ReduceM (Arg t) Source #

(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Abs a -> ReduceM (Abs a) Source #

InstantiateFull a => InstantiateFull (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

(Subst a, InstantiateFull a) => InstantiateFull (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull t => InstantiateFull (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull t => InstantiateFull (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

InstantiateFull t => InstantiateFull (WithArity t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

InstantiateFull t => InstantiateFull (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

InstantiateFull (Judgement MetaId) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Reduce

InstantiateFull t => InstantiateFull (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Maybe t -> ReduceM (Maybe t) Source #

InstantiateFull t => InstantiateFull (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Maybe t -> ReduceM (Maybe t) Source #

InstantiateFull t => InstantiateFull [t] Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: [t] -> ReduceM [t] Source #

InstantiateFull t => InstantiateFull (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Named name t -> ReduceM (Named name t) Source #

(InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Dom' t e -> ReduceM (Dom' t e) Source #

InstantiateFull t => InstantiateFull (Map k t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Map k t -> ReduceM (Map k t) Source #

InstantiateFull t => InstantiateFull (HashMap k t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: HashMap k t -> ReduceM (HashMap k t) Source #

(InstantiateFull a, InstantiateFull b) => InstantiateFull (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: (a, b) -> ReduceM (a, b) Source #

(InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: (a, b, c) -> ReduceM (a, b, c) Source #

(InstantiateFull a, InstantiateFull b, InstantiateFull c, InstantiateFull d) => InstantiateFull (a, b, c, d) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: (a, b, c, d) -> ReduceM (a, b, c, d) Source #

instantiateFullExceptForDefinitions :: MonadReduce m => Interface -> m Interface Source #

Instantiates everything except for definitions in the signature.

class IsMeta a Source #

Is something (an elimination of) a meta variable? Does not perform any reductions.

Minimal complete definition

isMeta

Instances

Instances details
IsMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Term -> Maybe MetaId Source #

IsMeta CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: CompareAs -> Maybe MetaId Source #

IsMeta a => IsMeta (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Arg a -> Maybe MetaId Source #

IsMeta a => IsMeta (Level' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Level' a -> Maybe MetaId Source #

IsMeta a => IsMeta (PlusLevel' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: PlusLevel' a -> Maybe MetaId Source #

IsMeta a => IsMeta (Sort' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Sort' a -> Maybe MetaId Source #

IsMeta a => IsMeta (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Elim' a -> Maybe MetaId Source #

IsMeta a => IsMeta (Type'' t a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Type'' t a -> Maybe MetaId Source #

isMeta :: IsMeta a => a -> Maybe MetaId Source #

class Reduce t Source #

Instances

Instances details
Reduce DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Type Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce UnifyState Source #

Don't ever reduce the whole varTel, as it will destroy readability of the context in interactive editing! To make sure this insight is not lost, the following dummy instance should prevent a proper Reduce instance for UnifyState.

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Unify.Types

Reduce t => Reduce (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Arg t -> ReduceM (Arg t) Source #

reduceB' :: Arg t -> ReduceM (Blocked (Arg t)) Source #

(Subst a, Reduce a) => Reduce (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Abs a -> ReduceM (Abs a) Source #

reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) Source #

Reduce t => Reduce (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Dom t -> ReduceM (Dom t) Source #

reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #

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

Defined in Agda.TypeChecking.Reduce

Reduce t => Reduce (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Primitive.Cubical.Base

Reduce t => Reduce (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Maybe t -> ReduceM (Maybe t) Source #

reduceB' :: Maybe t -> ReduceM (Blocked (Maybe t)) Source #

Reduce t => Reduce [t] Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: [t] -> ReduceM [t] Source #

reduceB' :: [t] -> ReduceM (Blocked [t]) Source #

Reduce e => Reduce (Map k e) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: Map k e -> ReduceM (Map k e) Source #

reduceB' :: Map k e -> ReduceM (Blocked (Map k e)) Source #

(Reduce a, Reduce b) => Reduce (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: (a, b) -> ReduceM (a, b) Source #

reduceB' :: (a, b) -> ReduceM (Blocked (a, b)) Source #

(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

reduce' :: (a, b, c) -> ReduceM (a, b, c) Source #

reduceB' :: (a, b, c) -> ReduceM (Blocked (a, b, c)) Source #

reduce' :: Reduce t => t -> ReduceM t Source #

reduce :: (Reduce a, MonadReduce m) => a -> m a Source #

reduceB :: (Reduce a, MonadReduce m) => a -> m (Blocked a) Source #

reduceDefCopy :: forall m. PureTCM m => QName -> Elims -> m (Reduced () Term) Source #

Reduce a non-primitive definition if it is a copy linking to another def.

reduceDefCopyTCM :: QName -> Elims -> TCM (Reduced () Term) Source #

Specialized version to put in boot file.

reduceHead :: PureTCM m => Term -> m (Blocked Term) Source #

Reduce simple (single clause) definitions.

unfoldInlined :: PureTCM m => Term -> m Term Source #

Unfold a single inlined function.

appDef' :: QName -> Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source #

Apply a defined function to it's arguments, using the original clauses.

abortIfBlocked :: (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) => t -> m t Source #

Throw pattern violation if blocked or a meta.

ifBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a Source #

Case on whether a term is blocked on a meta (or is a meta). That means it can change its shape when the meta is instantiated.

isBlocked :: (Reduce t, IsMeta t, MonadReduce m) => t -> m (Maybe Blocker) Source #

fromBlocked :: MonadBlock m => Blocked a -> m a Source #

Throw a pattern violation if the argument is Blocked, otherwise return the value embedded in the NotBlocked.

blockOnError :: MonadError TCErr m => Blocker -> m a -> m a Source #

Run the given computation but turn any errors into blocked computations with the given blocker

class Simplify t Source #

Only unfold definitions if this leads to simplification which means that a constructor/literal pattern is matched. We include reduction of IApply patterns, as `p i0` is akin to matcing on the i0 constructor of interval.

Instances

Instances details
Simplify EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Sort -> ReduceM Sort

Simplify Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Term -> ReduceM Term

Simplify Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Bool Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Bool -> ReduceM Bool

Simplify t => Simplify (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Arg t -> ReduceM (Arg t)

(Subst a, Simplify a) => Simplify (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Abs a -> ReduceM (Abs a)

Simplify t => Simplify (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Dom t -> ReduceM (Dom t)

(Subst a, Simplify a) => Simplify (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Tele a -> ReduceM (Tele a)

Simplify t => Simplify (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Type' t -> ReduceM (Type' t)

Simplify t => Simplify (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Elim' t -> ReduceM (Elim' t)

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

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Closure a -> ReduceM (Closure a)

Simplify t => Simplify (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify t => Simplify (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Maybe t -> ReduceM (Maybe t)

Simplify t => Simplify (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Maybe t -> ReduceM (Maybe t)

Simplify t => Simplify [t] Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: [t] -> ReduceM [t]

Simplify t => Simplify (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Named name t -> ReduceM (Named name t)

Simplify t => Simplify (Map k t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Map k t -> ReduceM (Map k t)

(Simplify a, Simplify b) => Simplify (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: (a, b) -> ReduceM (a, b)

(Simplify a, Simplify b, Simplify c) => Simplify (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: (a, b, c) -> ReduceM (a, b, c)

simplify :: (Simplify a, MonadReduce m) => a -> m a Source #

class Normalise t Source #

Instances

Instances details
Normalise ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Level Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Sort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Term Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Bool Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Bool -> ReduceM Bool Source #

Normalise Char Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Char -> ReduceM Char Source #

Normalise Int Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Int -> ReduceM Int Source #

Normalise t => Normalise (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Arg t -> ReduceM (Arg t) Source #

Normalise t => Normalise (WithHiding t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

(Subst a, Normalise a) => Normalise (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Abs a -> ReduceM (Abs a) Source #

Normalise t => Normalise (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Dom t -> ReduceM (Dom t) Source #

Normalise a => Normalise (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

(Subst a, Normalise a) => Normalise (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Tele a -> ReduceM (Tele a) Source #

Normalise t => Normalise (Type' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Type' t -> ReduceM (Type' t) Source #

Normalise t => Normalise (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Elim' t -> ReduceM (Elim' t) Source #

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

Defined in Agda.TypeChecking.Reduce

Normalise t => Normalise (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise t => Normalise (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Maybe t -> ReduceM (Maybe t) Source #

Normalise t => Normalise (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Maybe t -> ReduceM (Maybe t) Source #

Normalise t => Normalise [t] Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: [t] -> ReduceM [t] Source #

Normalise t => Normalise (Named name t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Named name t -> ReduceM (Named name t) Source #

Normalise t => Normalise (Map k t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Map k t -> ReduceM (Map k t) Source #

(Normalise a, Normalise b) => Normalise (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: (a, b) -> ReduceM (a, b) Source #

(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: (a, b, c) -> ReduceM (a, b, c) Source #

normalise :: (Normalise a, MonadReduce m) => a -> m a Source #