Expr representing a hole of Bool type.

> b_
_ :: Bool

Expr representing a variable p :: Bool.

> pp
p :: Bool

Expr representing a variable q :: Bool.

> qq
q :: Bool

Expr representing a variable r :: Bool.

> rr
r :: Bool

Expr representing a variable p' :: Bool.

> pp'
p' :: Bool

False encoded as an Expr.

> false
False :: Bool

True encoded as an Expr.

> true
True :: Bool

The function not encoded as an Expr.

> notE
not :: Bool -> Bool

The function or encoded as an Expr.

> orE
(||) :: Bool -> Bool -> Bool

The function and encoded as an Expr.

> andE
(&&) :: Bool -> Bool -> Bool

The ==> operator encoded as an Expr

The function not lifted over the Expr type.

> not' false
not False :: Bool

> evalBool $ not' false
True

> not' pp
not p :: Bool

The function || lifted over the Expr type.

> pp -||- qq
p || q :: Bool

> false -||- true
False || True :: Bool

> evalBool $ false -||- true
True

The function && lifted over the Expr type.

> pp -&&- qq
p && q :: Bool

> false -&&- true
False && True :: Bool

> evalBool $ false -&&- true
False

The function ==> lifted over Exprs.

> false -==>- true
False ==> True :: Bool

> evl $ false -==>- true :: Bool
True

Constructs an equation between two Exprs.

> xx -==- zero
x == 0 :: Bool

> cc -==- dee
c == 'd' :: Bool

This works for the Int, Bool, Char argument types and their lists.

Constructs an inequation between two Exprs.

> xx -/=- zero
x /= 0 :: Bool

> cc -/=- ae
c /= 'a' :: Bool

Constructs a less-than-or-equal inequation between two Exprs.

> xx -<=- zero
x <= 0 :: Bool

> cc -<=- ae
c <= 'a' :: Bool

Constructs a less-than inequation between two Exprs.

> xx -<- zero
x < 0 :: Bool

> cc -<- bee
c < 'b' :: Bool

Constructs an Expr-encoded compare operation between two Exprs.

> xx `compare'` zero
compare x 0 :: Ordering

> compare' ae bee
compare 'a' 'b' :: Ordering

A virtual function if :: Bool -> a -> a -> a lifted over the Expr type. This is displayed as an if-then-else.

> if' pp zero xx
(if p then 0 else x) :: Int

> zz -*- if' pp xx yy
z * (if p then x else y) :: Int

> if' pp false true -||- if' qq true false
(if p then False else True) || (if q then True else False) :: Bool

> evl $ if' true (val 't') (val 'f') :: Char
't'

A typed hole of Int type.

> i_
_ :: Int

A variable x of Int type.

> xx
x :: Int

A variable y of Int type.

> yy
y :: Int

A variable z of Int type.

> zz
z :: Int

A variable x' of Int type.

> xx'
x' :: Int

A variable i of Int type.

> ii
i :: Int

A variable j of Int type.

> jj
j :: Int

A variable k of Int type.

> kk
k :: Int

A variable i' of Int type.

> ii'
i' :: Int

A variable l of Int type.

> ll
l :: Int

A variable m of Int type.

> mm
m :: Int

A variable n of Int type.

> nn
n :: Int

The value 0 bound to the Int type encoded as an Expr.

> zero
0 :: Int

The value 1 bound to the Int type encoded as an Expr.

> one
1 :: Int

The value 2 bound to the Int type encoded as an Expr.

> two
2 :: Int

The value 3 bound to the Int type encoded as an Expr.

> three
3 :: Int

The value 4 bound to the Int type encoded as an Expr.

> four
4 :: Int

The value 5 bound to the Int type encoded as an Expr.

> five
5 :: Int

The value 6 bound to the Int type encoded as an Expr.

> six
6 :: Int

The value 7 bound to the Int type encoded as an Expr.

> seven
7 :: Int

The value 8 bound to the Int type encoded as an Expr.

> eight
8 :: Int

The value 9 bound to the Int type encoded as an Expr.

> nine
9 :: Int

The value 10 bound to the Int type encoded as an Expr.

> ten
10 :: Int

The value 11 bound to the Int type encoded as an Expr.

> eleven
11 :: Int

The value 12 bound to the Int type encoded as an Expr.

> twelve
12 :: Int

The value -1 bound to the Int type encoded as an Expr.

> minusOne
-1 :: Int

The value -2 bound to the Int type encoded as an Expr.

> minusOne
-2 :: Int

The function id for the Int type encoded as an Expr. (See also id'.)

> idE :$ xx
id x :: Int

> idE :$ zero
id 0 :: Int

> evaluate $ idE :$ zero :: Maybe Int
Just 0

negate over the Int type encoded as an Expr

> negateE
negate :: Int -> Int

abs over the Int type encoded as an Expr.

> absE
abs :: Int -> Int

signum over the Int type encoded as an Expr.

> signumE
signum :: Int -> Int

The function id encoded as an Expr. (cf. id')

The function id encoded as an Expr. (cf. id')

The function id encoded as an Expr. (cf. id')

The function id encoded as an Expr. (cf. id')

The function id encoded as an Expr. (cf. id')

The function id encoded as an Expr. (cf. id')

Constructs an application of id as an Expr. Only works for Int, Bool, Char, String, [Int], [Bool].

> id' yy
id yy :: Int

> id' one
id 1 :: Int

> evl (id' one) :: Int
1

> id' pp
id p :: Bool

> id' false
id' False :: Bool

> evl (id' true) :: Bool
True :: Bool

The const function lifted over the Expr type.

> const' zero one
const 0 1 :: Int

This works for the argument types Int, Char, Bool and their lists.

negate over the Int type lifted over the Expr type.

> negate' xx
negate x :: Int

> evl (negate' one) :: Int
-1

abs over the Int type lifted over the Expr type.

> abs' xx'
abs x' :: Int

> evl (abs' minusTwo) :: Int
2

signum over the Int type lifted over the Expr type.

> signum' xx'
signum x' :: Int

> evl (signum' minusTwo) :: Int
-1

The operator + for the Int type. (See also -+-.)

> plus
(+) :: Int -> Int -> Int

> plus :$ one
(1 +) :: Int -> Int

> plus :$ xx :$ yy
x + y :: Int

The operator * for the Int type. (See also -*-.)

> times
(*) :: Int -> Int -> Int

> times :$ two
(2 *) :: Int -> Int

> times :$ xx :$ yy
x * y :: Int

The subtraction - operator encoded as an Expr.

> minus :$ one
(1 -) :: Int -> Int

> minus :$ one :$ zero
1 - 0 :: Int

The operator + for the Int type for use on Exprs. (See also plus.)

> two -+- three
2 + 3 :: Int

> minusOne -+- minusTwo -+- zero
((-1) + (-2)) + 0 :: Int

> xx -+- (yy -+- zz)
x + (y + z) :: Int

The operator * for the Int type lifted over the Expr type. (See also times.)

> three -*- three
3 * 3 :: Int

> one -*- two -*- three
(1 * 2) * 3 :: Int

> two -*- xx
2 * x :: Int

Integer division div encoded as an Expr.

> divE :$ two
(2 `div`) :: Int -> Int

> divE :$ two :$ three
2 `div` 3 :: Int

Integer modulo mod encoded as an Expr.

> modE :$ two
(2 `mod`) :: Int -> Int

> modE :$ two :$ three
2 `mod` 3 :: Int

Integer quotient quot encoded as an Expr.

> quotE :$ two
(2 `quot`) :: Int -> Int

> quotE :$ two :$ three
2 `quot` 3 :: Int

Integer remainder rem encoded as an Expr.

> remE :$ two
(2 `rem`) :: Int -> Int

> remE :$ two :$ three
2 `rem` 3 :: Int

The function div for the Int type lifted over the Expr type. (See also mod.)

> six `div'` four
6 `div` 4 :: Int

The function mod for the Int type lifted over the Expr type. (See also div.)

> six `mod'` four
6 `mod` 4 :: Int

The function quot for the Int type lifted over the Expr type. (See also rem.)

> six `quot'` four
6 `quot` 4 :: Int

The function rem for the Int type lifted over the Expr type. (See also quot.)

> six `rem'` four
6 `rem` 4 :: Int

A variable function f of 'Int -> Int' type lifted over the Expr type.

> ff xx
f x :: Int

> ff one
f 1 :: Int

A variable f of 'Int -> Int' type encoded as an Expr.

> ffE
f :: Int -> Int

A variable function g of 'Int -> Int' type lifted over the Expr type.

> gg yy
g y :: Int

> gg minusTwo
gg (-2) :: Int

A variable g of 'Int -> Int' type encoded as an Expr.

> ggE
g :: Int -> Int

A variable function h of 'Int -> Int' type lifted over the Expr type.

> hh zz
h z :: Int

A variable h of 'Int -> Int' type encoded as an Expr.

> hhE
h :: Int -> Int

A variable binary operator o lifted over the Expr type. Works for Int, Bool, Char, [Int] and String.

> xx `oo` yy
x `o` y :: Int

> pp `oo` qq
p `o` q :: Bool

> xx `oo` qq
*** Exception: (-?-): cannot apply `o :: * -> * -> *` to `x :: Int' and `q :: Bool'.  Unhandled types?

A variable binary function o encoded as an Expr (cf. oo)

> ooE :$ xx :$ yy
x `o` y :: Int

> ooE :$ pp :$ qq
p `o` q :: Bool

A variable binary operator ? encoded as an Expr (cf. -?-)

> question :$ xx :$ yy
x ? y :: Int

> question :$ pp :$ qq
p ? q :: Bool

A variable binary operator ? lifted over the Expr type. Works for Int, Bool, Char, [Int] and String.

> xx -?- yy
x ? y :: Int

> pp -?- qq
p ? q :: Bool

> xx -?- qq
*** Exception: (-?-): cannot apply `(?) :: * -> * -> *` to `x :: Int' and `q :: Bool'.  Unhandled types?

$ lifted over Exprs

> absE -$- one
abs $ 1 :: Int

Works for Int, Bool, Char argument types and their lists.

odd with an Int argument lifted over the Expr type.

> odd' (xx -+- one)
odd (x + 1) :: Bool

> evl (odd' two) :: Bool
False

even with an Int argument lifted over the Expr type.

> even' (xx -+- two)
even (x + 2) :: Bool

> evl (even' two) :: Bool
True

A hole of Char type encoded as an Expr.

> c_
_ :: Char

A hole of String type encoded as an Expr.

> cs_
_ :: [Char]

A variable named c of type Char encoded as an Expr.

> cc
c :: Char

A variable named c of type Char encoded as an Expr.

> dd
d :: Char

A variable named cs of type String encoded as an Expr.

> ccs
cs :: [Char]

The character 'a' encoded as an Expr.

> ae
'a' :: Char

> evl ae :: Char
'a'

The character 'b' encoded as an Expr

> bee
'b' :: Char

> evl bee :: Char
'b'

The character 'c' encoded as an Expr

> cee
'c' :: Char

> evl cee :: Char
'c'

The character 'd' encoded as an Expr

> dee
'd' :: Char

> evl dee :: Char
'd'

The character 'z' encoded as an Expr

> zed
'z' :: Char

> evl zed :: Char
'z'

(cf. zee)

The character 'z' encoded as an Expr

> zee
'z' :: Char

> evl zee :: Char
'z'

(cf. zed)

The space character encoded as an Expr

> space
' ' :: Char

The line break character encoded as an Expr

> lineBreak
'\n' :: Char

The ord function lifted over Expr

> ord' bee
ord 'b' :: Int

> evl (ord' bee)
98

The ord function encoded as an Expr

A typed hole of [Int] type encoded as an Expr.

> is_
_ :: [Int]

A variable named xs of type [Int] encoded as an Expr.

> xxs
xs :: [Int]

A variable named ys of type [Int] encoded as an Expr.

> yys
ys :: [Int]

A variable named zs of type [Int] encoded as an Expr.

> yys
ys :: [Int]

An empty list of type [Int] encoded as an Expr.

> nil
[] :: [Int]

An empty String encoded as an Expr.

> emptyString
"" :: String

The empty list '[]' encoded as an Expr.

The empty list '[]' encoded as an Expr.

The empty list '[]' encoded as an Expr.

The list constructor with Int as element type encoded as an Expr.

> cons
(:) :: Int -> [Int] -> [Int]

> cons :$ one :$ nil
[1] :: [Int]

Consider using -:- and unit when building lists of Expr.

The list constructor : encoded as an Expr.

The list constructor : encoded as an Expr.

The list constructor : encoded as an Expr.

The list constructor lifted over the Expr type. Works for the element types Int, Char and Bool.

> zero -:- one -:- unit two
[0,1,2] :: [Int]

> zero -:- one -:- two -:- nil
[0,1,2] :: [Int]

> bee -:- unit cee
"bc" :: [Char]

unit constructs a list with a single element. This works for elements of type Int, Char and Bool.

> unit one
[1]

> unit false
[False]

List concatenation lifted over the Expr type. Works for the element types Int, Char and Bool.

> (zero -:- one -:- nil) -:- (two -:- three -:- nil)
[0,1] -++- [2,3] :: [Int]

> (bee -:- unit cee) -:- unit dee
"bc" -++- "c" :: [Char]

List head lifted over the Expr type. Works for the element types Int, Char and Bool.

> head' $ unit one
head [1] :: Int

> head' $ unit bee
head "b" :: Char

> head' $ zero -:- unit two
head [0,2] :: Int

> evl $ head' $ unit one :: Int
1

List tail lifted over the Expr type. Works for the element types Int, Char and Bool.

> tail' $ unit one
tail [1] :: [Int]

> tail' $ unit bee
tail "b" :: [Char]

> tail' $ zero -:- unit two
tail [0,2] :: [Int]

> evl $ tail' $ zero -:- unit two :: [Int]
[2]

List null lifted over the Expr type. Works for the element types Int, Char and Bool.

> null' $ unit one
null [1] :: Bool

> null' $ nil
null [] :: Bool

> evl $ null' nil :: Bool
True

List length lifted over the Expr type. Works for the element types Int, Char and Bool.

> length' $ unit one
length [1] :: Int

> length' $ unit bee
length "b" :: Int

> length' $ zero -:- unit two
length [0,2] :: Int

> evl $ length' $ unit one :: Int
1

List init lifted over the Expr type. Works for the element types Int, Char and Bool.

> init' $ unit one
init [1] :: [Int]

> init' $ unit bee
init "b" :: [Char]

> init' $ zero -:- unit two
init [0,2] :: [Int]

> evl $ init' $ zero -:- unit two :: [Int]
[0]

List elem lifted over the Expr type. Works for the element types Int, Char and Bool.

> elem' false (false -:- unit true)
elem False [False,True] :: Bool

> evl $ elem' false (false -:- unit true) :: Bool
True

List sort lifted over the Expr type. Works for the element types Int, Char and Bool.

> sort' $ unit one
sort [1] :: Int

> sort' $ unit bee
sort "b" :: Int

> sort' $ zero -:- unit two
sort [0,2] :: Int

> evl $ sort' $ two -:- unit one :: [Int]
[1,2]

List insert lifted over the Expr type. Works for the element types Int, Char and Bool.

> insert' zero nilInt
insert 0 [] :: [Int]

> insert' false (false -:- unit true)
insert False [False,True] :: [Bool]

A typed hole of [Bool] type encoded as an Expr.

> bs_
_ :: [Bool]

Expr representing a variable p' :: `[Bool]`.

> pps
ps :: [Bool]

A typed hole of '[Bool]' type

> qqs
qs :: [Bool]

and lifted over the Expr type.

> and' pps
and ps :: Bool

> evl (and' $ expr [False,True]) :: Bool
False

or lifted over the Expr type.

> or' pps
or ps :: Bool

> evl (or' $ expr [False,True]) :: Bool
True

sum of Int elements lifted over the Expr type.

> sum' xxs
sum xs :: Int

> evl (sum' $ expr [1,2,3::Int]) :: Int
6

product of Int elements lifted over the Expr type.

> product' xxs
product xs :: Int

> evl (product' $ expr [1,2,3::Int]) :: Int
6

Append for list of Ints encoded as an Expr.

Nothing bound to the Maybe Int type encoded as an Expr.

This is an alias to nothingInt.

Nothing bound to the Maybe Int type encoded as an Expr.

Nothing bound to the Maybe Bool type encoded as an Expr.

The Just constructor lifted over the Expr type.

This works for the Bool and Int argument types.

> just zero
Just 0 :: Maybe Int
> just false
Just False :: Maybe Bool

The Just constructor of the Int element type encoded as an Expr.

The Just constructor of the Bool element type encoded as an Expr.

The pair constructor ( :: ... -> (Int,Int) ) encoded as an Expr.

The pair constructor lifted over Exprs.

This works for the Int and Bool element types by differently from foldPair by returning a well-typed expression.

An infix synonym of pair.

The triple/trio constructor lifted over Exprs.

This only works for the Int element type.

The quadruple constructor lifted over Exprs.

This only works for the Int element type.

The quintuple constructor lifted over Exprs.

This only works for the Int element type.

The sixtuple constructor lifted over Exprs.

This only works for the Int element type.

The % constructor lifted over Exprs.

> val (2 :: Integer) -%- val (3 :: Integer)
2 % 3 :: Ratio Integer

This only accepts Exprs bound to the Integer type.

Function composition encoded as an Expr:

> compose
(.) :: (Int -> Int) -> (Int -> Int) -> Int -> Int

map over the Int element type encoded as an Expr

> mapE
map :: (Int -> Int) -> [Int] -> [Int]

Function composition . lifted over Expr.

> absE -.- negateE
abs . negate :: Int -> Int

> absE -.- negateE :$ one
(abs . negate) 1 :: Int

This works for Int, Bool, Char and their lists.

map lifted over Exprs.

> map' absE (unit one)
map abs [1] :: [Int]

enumFrom lifted over Exprs.

> enumFrom' zero
enumFrom 0 :: [Int]

Works for Ints, Bools and Chars.

enumFrom lifted over Exprs named as ".." for pretty-printing.

> (-..) one
[1..] :: [Int]

Works for Ints, Bools and Chars.

enumFromTo lifted over Exprs

> enumFromTo' zero four
enumFromTo 0 4 :: [Int]

enumFromTo lifted over Exprs but named as ".." for pretty-printing.

> zero -..- four
[0..4] :: [Int]

enumFromThen lifted over Exprs

> enumFromThen' zero ten
enumFromThen 0 10 :: [Int]

enumFromThen lifted over Exprs but named as ",.." for pretty printing.

> zero -... ten
[0,10..] :: [Int]

enumFromThenTo lifted over Exprs.

> enumFromThenTo' zero two ten
enumFromThenTo 0 2 10 :: [Int]

enumFromThenTo lifted over Exprs but named as ",.." for pretty-printing.

> (zero -...- two) ten
[0,2..10] :: [Int]