lambda-cube-0.3.0: Some thoughts on Calculus of Constructions
Safe HaskellNone
LanguageHaskell2010

L3.Core.Eq

Description

Type checking and type inference

Synopsis

Documentation

alphaEq :: (Eq a, Enum a, Show a) => Expr a -> Expr a -> Bool Source #

Deduce whether two expressions are equivalent by converting to indexed form and checking for exact equality. This does not apply normalisation, so represents only alpha-equivalence of expressions.

betaEq :: (Eq a, Enum a, Show a) => Expr a -> Expr a -> Bool Source #

Deduce whether two expressions are equivalent by converting to indexed form and checking for exact equality. This does apply normalisation, so represents beta-equivalence (and implicitly alpha-equivalence) of expressions.