Closed L-as closed 1 year ago
type family T :: forall (edsl :: EDSLKind). EType -> Type type family T a where T @edsl a = Term edsl a
This is useful for annotating types inside terms
An alternative:
phe :: forall a edsl. Term edsl a -> Term edsl a phe = id x :: PConstructable edsl PBool => Term edsl PBool x = phe @PBool $ pcon ETrue
Fixed
This is useful for annotating types inside terms