Safe Haskell | None |
---|---|
Language | Haskell2010 |
Documentation
Show Ty Source # | |
Rep Ty Source # | |
Alpha Ty Source # | |
Display Ty Source # | |
(Sat (ctx0 TyName), Sat (ctx0 (Bind [TyName] [Ty])), Sat (ctx0 [Ty]), Sat (ctx0 (Bind TyName Ty))) => Rep1 ctx0 Ty Source # | |
Subst Val Ty Source # | |
Subst Ty Prim Source # | |
Subst Ty Tm Source # | |
Subst Ty Decl Source # | |
Subst Ty AnnVal Source # | |
Subst Ty Val Source # | |
Subst Ty Ty Source # | |
Display (ValName, Embed Ty) Source # | |
TmInt Int | |
TmVar ValName | |
Fix (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm)) | |
TmProd [AnnVal] | |
TApp AnnVal Ty | |
Pack Ty AnnVal |
Show Val Source # | |
Rep Val Source # | |
Alpha Val Source # | |
Display Val Source # | |
(Sat (ctx0 Int), Sat (ctx0 ValName), Sat (ctx0 (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm))), Sat (ctx0 [AnnVal]), Sat (ctx0 AnnVal), Sat (ctx0 Ty)) => Rep1 ctx0 Val Source # | |
Subst Val Prim Source # | |
Subst Val Tm Source # | |
Subst Val Decl Source # | |
Subst Val AnnVal Source # | |
Subst Val Val Source # | |
Subst Val Ty Source # | |
Subst Ty Val Source # | |
Display (ValName, Embed Ty) Source # | |
rTm1 :: forall ctx. ctx (Bind Decl Tm) -> (ctx AnnVal, ctx [AnnVal]) -> (ctx AnnVal, ctx Tm, ctx Tm) -> (ctx Ty, ctx AnnVal) -> R1 ctx Tm Source #
rDecl1 :: forall ctx. (ctx ValName, ctx (Embed AnnVal)) -> (ctx Int, ctx ValName, ctx (Embed AnnVal)) -> (ctx ValName, ctx (Embed (AnnVal, Prim, AnnVal))) -> (ctx TyName, ctx ValName, ctx (Embed AnnVal)) -> R1 ctx Decl Source #
rVal1 :: forall ctx. ctx Int -> ctx ValName -> ctx (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm)) -> ctx [AnnVal] -> (ctx AnnVal, ctx Ty) -> (ctx Ty, ctx AnnVal) -> R1 ctx Val Source #