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




findIdx :: Eq a => [a] -> a -> Maybe IntSource

Find position of a value in a list. Used to change metavar argument indices during assignment.

reverse is necessary because we are directly abstracting over the list.

isBlockedTerm :: MonadTCM tcm => MetaId -> tcm BoolSource

Check whether a meta variable is a place holder for a blocked term.

(=:=) :: MonadTCM tcm => MetaId -> Term -> tcm ()Source

(=:) :: (MonadTCM tcm, HasMeta t, KillRange t, Show t) => MetaId -> t -> tcm ()Source

The instantiation should not be an InstV or InstS and the MetaId should point to something Open or a BlockedConst.

assignTerm :: MonadTCM tcm => MetaId -> Term -> tcm ()Source

assignSort :: MonadTCM tcm => MetaId -> Sort -> tcm ()Source

newValueMeta :: MonadTCM tcm => Type -> tcm TermSource

Create a new metavariable, possibly -expanding in the process.

newValueMeta' :: MonadTCM tcm => Type -> tcm TermSource

Create a new value meta without -expanding.

newValueMetaCtx' :: MonadTCM tcm => Type -> Args -> tcm TermSource

Create a new value meta with specific dependencies.

newRecordMeta :: MonadTCM tcm => QName -> Args -> tcm TermSource

Create a metavariable of record type. This is actually one metavariable for each field.

blockTerm :: MonadTCM tcm => Type -> Term -> tcm Constraints -> tcm TermSource

Construct a blocked constant if there are constraints.

unblockedTester :: MonadTCM tcm => Type -> tcm BoolSource

Auxiliary function to create a postponed type checking problem.

etaExpandListeners :: MonadTCM tcm => MetaId -> tcm ()Source

Eta expand metavariables listening on the current meta.

etaExpandMetaSafe :: MonadTCM tcm => MetaId -> tcm ()Source

Do safe eta-expansions for meta (SingletonRecords,Levels).

data MetaKind Source

Various kinds of metavariables.



Meta variables of record type.


Meta variables of "hereditarily singleton" record type.


Meta variables of level type, if type-in-type is activated.

allMetaKinds :: [MetaKind]Source

All possible metavariable kinds.

etaExpandMeta :: MonadTCM tcm => [MetaKind] -> MetaId -> tcm ()Source

Eta expand a metavariable, if it is of the specified kind. Don't do anything if the metavariable is a blocked term.

etaExpandBlocked :: (MonadTCM tcm, Reduce t) => Blocked t -> tcm (Blocked t)Source

Eta expand blocking metavariables of record type, and reduce the blocked thing.

abortAssign :: MonadTCM tcm => tcm aSource

handleAbort :: MonadTCM tcm => TCM a -> TCM a -> tcm aSource

assignV :: MonadTCM tcm => Type -> MetaId -> Args -> Term -> tcm ConstraintsSource

Assign to an open metavar. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.

checkArgs :: MonadTCM tcm => MetaId -> Args -> FVs -> tcm [Arg Nat]Source

Check that arguments to a metavar are in pattern fragment. Assumes all arguments already in whnf. Parameters are represented as Vars so checkArgs really checks that all args are unique Vars and returns the list of corresponding indices for each arg-- done to not define equality on Term.

reverse is necessary because we are directly abstracting over this list ids.

validParameters :: Monad m => Args -> FVs -> m [Arg Nat]Source

Check that the parameters to a meta variable are distinct variables. Andreas, 2010-09-24: Allow non-linear variables that do not appear in FVs.

updateMeta :: (MonadTCM tcm, Data a, Occurs a, Abstract a) => MetaId -> a -> tcm ()Source