-
Notifications
You must be signed in to change notification settings - Fork 0
/
pretty.txt
34 lines (30 loc) · 993 Bytes
/
pretty.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
max expr size = 7
|- on ineqs = 6
|- on conds = 6
max #-tests = 500
min #-tests = 25 (to consider p ==> q true)
max #-vars = 3 (for inequational and conditional laws)
_ :: Char
_ :: Doc
_ :: Int
_ :: [Char]
($$) :: Doc -> Doc -> Doc
(<>) :: Doc -> Doc -> Doc
nest :: Int -> Doc -> Doc
(++) :: [Char] -> [Char] -> [Char]
length :: [Char] -> Int
d1 <> nest x d2 == d1 <> d2
(d1 $$ d2) $$ d3 == d1 $$ (d2 $$ d3)
(d1 <> d2) <> d3 == d1 <> (d2 <> d3)
nest x (nest y d1) == nest y (nest x d1)
(d1 $$ d2) <> d3 == d1 $$ (d2 <> d3)
nest x (d1 <> d2) == nest x d1 <> d2
d1 <> (nest x d2 <> d3) == d1 <> (d2 <> d3)
nest x (d1 $$ d2) == nest x d1 $$ nest x d2
nest (length (cs ++ ds)) d1 == nest (length cs) (nest (length ds) d1)
d1 <= d1 $$ d2
d1 <= d1 <> d2
d1 $$ d2 <= d1 $$ (d2 $$ d3)
d1 <> d2 <= d1 <> (d2 <> d3)
d1 $$ d2 <= d1 $$ (d2 <> d3)
d1 <> d2 <= d1 <> (d2 $$ d3)