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])) => 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] |
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])) => 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 [Ty], 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))) -> R1 ctx Decl Source #