{"body":"type Vec :: Type -> Nat -> Type\ntype role Vec representational nominal\ndata Vec a n where\n  VNil  :: Vec a Z\n  VCons :: a -> Vec a n -> Vec a (S n)\n\ntype SVec0 :: forall a n. Vec a n -> Type\ntype role SVec0 nominal\ndata SVec0 a where\n  SVNil0 :: SVec0 'VNil\n  SVCons0 :: Sing a -> SVec0 b -> SVec0 ('VCons a b)","name":"svec0","extension":"txt","url":"https://www.irccloud.com/pastebin/j3dAUDko/svec0","modified":1600603667,"id":"j3dAUDko","size":310,"lines":11,"own_paste":false,"theme":"","date":1600603667}