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

L3.Core.Normal

Description

Type checking and type inference

Synopsis

Documentation

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

Is a name free in an expression In this context, free v a & v = v' => substitute v v' a = a i.e. would a substitution be performed

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

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

Substitute all occurrences of a variable v with an expression e. substitute v e E ~ E[v := e]

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

Given an expression, reduce it one step towards its normal form.

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

Given an expression, totally reduce it over all steps towards normal form.