Safe Haskell | None |
---|---|
Language | Haskell2010 |
EDSL to construct terms without touching De Bruijn indices.
e.g. if given t, u :: Term, Γ ⊢ t, u : A, we can build "λ f. f t u" like this:
runNames [] $ do
-- open
binds t
and u
to computations that know how to weaken themselves in
-- an extended context
- t,u
- <- mapM open [t,u]
- -
lam
gives the illusion of HOAS by providing f as a computation - - It also extends the internal context with the name "f", so that
- -
t
andu
will get weakened in the body. - - Then we finish the job using the (@) combinator from Agda.TypeChecking.Primitive
Documentation
Instances
MonadTrans NamesT Source # | |
Defined in Agda.TypeChecking.Names | |
MonadState s m => MonadState s (NamesT m) Source # | |
Monad m => Monad (NamesT m) Source # | |
Functor m => Functor (NamesT m) Source # | |
MonadFail m => MonadFail (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names | |
Applicative m => Applicative (NamesT m) Source # | |
MonadIO m => MonadIO (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names | |
MonadTCM m => MonadTCM (NamesT m) Source # | |
MonadTCState m => MonadTCState (NamesT m) Source # | |
MonadTCEnv m => MonadTCEnv (NamesT m) Source # | |
MonadReduce m => MonadReduce (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names liftReduce :: ReduceM a -> NamesT m a Source # | |
HasOptions m => HasOptions (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names | |
ReadTCState m => ReadTCState (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names | |
MonadDebug m => MonadDebug (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names | |
HasBuiltins m => HasBuiltins (NamesT m) Source # | |
Defined in Agda.TypeChecking.Names |
cl' :: Applicative m => a -> NamesT m a Source #
bind' :: (Monad m, Subst t' b, DeBruijn b, Subst t a, Free a) => ArgName -> (NamesT m b -> NamesT m a) -> NamesT m a Source #
bind :: (Monad m, Subst t' b, DeBruijn b, Subst t a, Free a) => ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a) Source #