diff options
| -rw-r--r-- | src/SOAS.idr | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/SOAS.idr b/src/SOAS.idr index 8540c83..80c5f7f 100644 --- a/src/SOAS.idr +++ b/src/SOAS.idr @@ -151,6 +151,13 @@ record (.PointedCoalgStruct) type (x : type.SortedFamily) where ren : x -|> [] x var : Var -|> x +%hint +(.VarPointedCoalgStruct) : (0 type : Type) -> type.PointedCoalgStruct Var +type.VarPointedCoalgStruct = MkPointedCoalgStruct + { ren = \i, f => f i + , var = id + } + liftPos : (ctx : type.Ctx) -> (mon : type.PointedCoalgStruct p) => {ctx2 : type.Ctx} -> (p.subst ctx1 ctx2) -> p.substNamed (ctx1 ++ ctx) (ctx2 ++ ctx) |