diff options
Diffstat (limited to 'src/AST.hs')
-rw-r--r-- | src/AST.hs | 12 |
1 files changed, 9 insertions, 3 deletions
@@ -285,9 +285,15 @@ mapExt f = \case EOneHot x t p a b -> EOneHot (f x) t p (mapExt f a) (mapExt f b) EError x t s -> EError (f x) t s -subst1 :: Expr x env a -> Expr x (a : env) t -> Expr x env t -subst1 repl = subst $ \x t -> \case IZ -> repl - IS i -> EVar x t i +substInline :: Expr x env a -> Expr x (a : env) t -> Expr x env t +substInline repl = + subst $ \x t -> \case IZ -> repl + IS i -> EVar x t i + +subst0 :: Ex (b : env) a -> Ex (a : env) t -> Ex (b : env) t +subst0 repl = + subst $ \_ t -> \case IZ -> repl + IS i -> EVar ext t (IS i) subst :: (forall a. x a -> STy a -> Idx env a -> Expr x env' a) -> Expr x env t -> Expr x env' t |