Safe Haskell	None
Language	Haskell2010

KleenePlugin.Synthesis

Description

Core synthesis.

We transform from our types to CoreExpr or Type. The code is very direct, but we have to provide everything (type and coercion arguments!) manually.

Synopsis

synStrType :: [Type] -> Type
synSList :: KleNames -> [Type] -> CoreExpr
synProof :: FamInstEnvs -> KleNames -> Proof Coercion Type Type -> CoreExpr
synReType :: KleNames -> RE Type -> Type

Documentation

synStrType :: [Type] -> Type Source #

synthesise type level list (of types).

synSList :: KleNames -> [Type] -> CoreExpr Source #

synthesise SList value.

synProof :: FamInstEnvs -> KleNames -> Proof Coercion Type Type -> CoreExpr Source #

synthesise Match from Proof.

synReType :: KleNames -> RE Type -> Type Source #

Synthesise type level RE (of types).