free-compiler-0.3.0.0: A Haskell to Coq compiler.

Safe HaskellNone
LanguageHaskell2010

FreeC.Backend.Agda.Converter.Expr

Description

Implements the lifted IR to Agda translation for expressions.

Synopsis

Documentation

convertLiftedExpr :: Expr -> Converter Expr Source #

Converts an expression from lifted IR to an Agda expression.