2
1
module Agda.TypeChecking.MetaVars where
4
import Agda.Syntax.Internal ( MetaId, Term, Type, Args, Abs, Dom, Telescope )
3
import Agda.Syntax.Internal ( MetaId, Term, Type, Arg, Args, Abs, Dom, Telescope )
4
import Agda.Syntax.Internal.Generic ( TermLike )
5
5
import Agda.TypeChecking.Monad.Base ( TCM, RunMetaOccursCheck(..), CompareDirection(..) )
7
7
type Condition = Dom Type -> Abs Type -> Bool
8
8
newArgsMeta' :: Condition -> Type -> TCM Args
9
9
newArgsMeta :: Type -> TCM Args
10
assignTerm :: MetaId -> Term -> TCM ()
10
assignTerm :: MetaId -> [Arg String] -> Term -> TCM ()
11
11
etaExpandMetaSafe :: MetaId -> TCM ()
12
12
assignV :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
13
assign :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
14
newIFSMeta :: String -> Type -> [(Term, Type)] -> TCM Term
13
assign :: CompareDirection -> MetaId -> Args -> Term -> TCM ()
14
newIFSMeta :: String -> Type -> Maybe [(Term, Type)] -> TCM Term
15
15
newValueMeta :: RunMetaOccursCheck -> Type -> TCM Term
16
16
newNamedValueMeta :: RunMetaOccursCheck -> String -> Type -> TCM Term
17
17
newTelMeta :: Telescope -> TCM Args
18
allMetas :: TermLike a => a -> [MetaId]
added
removed
src/full/Agda/TypeChecking/MetaVars.hs-boot
