-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathBasicsTest1.hs.html
109 lines (108 loc) · 25.2 KB
/
BasicsTest1.hs.html
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<html>
<head>
<title>/home/michael/liquidmeta_public/BasicsTest1.hs</title>
</head>
<head>
<link type='text/css' rel='stylesheet' href='liquid.css' />
</head>
<body>
<hr>
Put mouse over identifiers to see inferred types
<pre><span class=hs-linenum> 1: </span><a class=annot href="#"><span class=annottext>GHC.Types.Module</span><span class='hs-comment'>{-# LANGUAGE GADTs #-}</span></a>
<span class=hs-linenum> 2: </span>
<span class=hs-linenum> 3: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--reflection"</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum> 4: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--ple"</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum> 5: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--short-names"</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum> 6: </span>
<span class=hs-linenum> 7: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>BasicsTest1</span> <span class='hs-keyword'>where</span>
<span class=hs-linenum> 8: </span>
<span class=hs-linenum> 9: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Prelude</span> <span class='hs-varid'>hiding</span> <span class='hs-layout'>(</span><span class='hs-varid'>max</span><span class='hs-layout'>)</span>
<span class=hs-linenum>10: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Language.Haskell.Liquid.ProofCombinators</span> <span class='hs-varid'>hiding</span> <span class='hs-layout'>(</span><span class='hs-varid'>withProof</span><span class='hs-layout'>)</span>
<span class=hs-linenum>11: </span><span class='hs-keyword'>import</span> <span class='hs-keyword'>qualified</span> <span class='hs-conid'>Data.Set</span> <span class='hs-keyword'>as</span> <span class='hs-conid'>S</span>
<span class=hs-linenum>12: </span>
<span class=hs-linenum>13: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>measure</span> <span class='hs-varid'>propOf</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>b</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>14: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>ProofOf</span> <span class='hs-conid'>E</span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>{</span> <span class='hs-varid'>proofObj</span><span class='hs-conop'>:</span><span class='hs-keyword'>_</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>propOf</span> <span class='hs-varid'>proofObj</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>E</span> <span class='hs-layout'>}</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>15: </span>
<span class=hs-linenum>16: </span><span class='hs-comment'>---------------------------------------------------------------------------</span>
<span class=hs-linenum>17: </span><span class='hs-comment'>----- | TERMS of our language</span>
<span class=hs-linenum>18: </span><span class='hs-comment'>---------------------------------------------------------------------------</span>
<span class=hs-linenum>19: </span><span class='hs-keyword'>type</span> <span class='hs-conid'>Vname</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>20: </span>
<span class=hs-linenum>21: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>Basic</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>TBool</span> <span class='hs-comment'>-- Bool</span>
<span class=hs-linenum>22: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>TInt</span> <span class='hs-comment'>-- Int</span>
<span class=hs-linenum>23: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>BTV</span> <span class='hs-conid'>Vname</span> <span class='hs-comment'>-- a -- NEW!</span>
<span class=hs-linenum>24: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>FTV</span> <span class='hs-conid'>Vname</span> <span class='hs-comment'>-- a -- NEW!</span>
<span class=hs-linenum>25: </span> <span class='hs-keyword'>deriving</span> <span class='hs-layout'>(</span><span class='hs-conid'>Eq</span><span class='hs-layout'>,</span> <span class='hs-conid'>Show</span><span class='hs-layout'>)</span>
<span class=hs-linenum>26: </span>
<span class=hs-linenum>27: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>Kind</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Base</span> <span class='hs-comment'>-- B, base kind</span>
<span class=hs-linenum>28: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>Star</span> <span class='hs-comment'>-- *, star kind</span>
<span class=hs-linenum>29: </span> <span class='hs-keyword'>deriving</span> <span class='hs-layout'>(</span><span class='hs-conid'>Eq</span><span class='hs-layout'>,</span> <span class='hs-conid'>Show</span><span class='hs-layout'>)</span>
<span class=hs-linenum>30: </span>
<span class=hs-linenum>31: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>FType</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>FTBasic</span> <span class='hs-conid'>Basic</span> <span class='hs-comment'>-- b: Bool, Int, FTV a, BTV a</span>
<span class=hs-linenum>32: </span> <span class='hs-keyword'>deriving</span> <span class='hs-layout'>(</span><span class='hs-conid'>Eq</span><span class='hs-layout'>,</span> <span class='hs-conid'>Show</span><span class='hs-layout'>)</span>
<span class=hs-linenum>33: </span>
<span class=hs-linenum>34: </span> <span class='hs-comment'>--- TYPING ENVIRONMENTS</span>
<span class=hs-linenum>35: </span>
<span class=hs-linenum>36: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>FEmpty</span> <span class='hs-comment'>-- type FEnv = [(Vname, FType) or Vname]</span>
<span class=hs-linenum>37: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>FCons</span> <span class='hs-conid'>Vname</span> <span class='hs-conid'>FType</span> <span class='hs-conid'>FEnv</span>
<span class=hs-linenum>38: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>FConsT</span> <span class='hs-conid'>Vname</span> <span class='hs-conid'>Kind</span> <span class='hs-conid'>FEnv</span>
<span class=hs-linenum>39: </span> <span class='hs-keyword'>deriving</span> <span class='hs-layout'>(</span><span class='hs-conid'>Show</span><span class='hs-layout'>)</span>
<span class=hs-linenum>40: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>data</span> <span class='hs-conid'>FEnv</span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>41: </span> <span class='hs-conid'>FEmpty</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>FEnv</span>
<span class=hs-linenum>42: </span> <span class='hs-conid'>FCons</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-conid'>Vname</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>t</span><span class='hs-conop'>:</span><span class='hs-conid'>FType</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>{</span> <span class='hs-varid'>g</span><span class='hs-conop'>:</span><span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>not</span> <span class='hs-layout'>(</span><span class='hs-varid'>in_envF</span> <span class='hs-varid'>x</span> <span class='hs-varid'>g</span><span class='hs-layout'>)</span> <span class='hs-layout'>}</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>FEnv</span>
<span class=hs-linenum>43: </span> <span class='hs-conid'>FConsT</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-conop'>:</span><span class='hs-conid'>Vname</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>k</span><span class='hs-conop'>:</span><span class='hs-conid'>Kind</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>{</span> <span class='hs-varid'>g</span><span class='hs-conop'>:</span><span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>not</span> <span class='hs-layout'>(</span><span class='hs-varid'>in_envF</span> <span class='hs-varid'>a</span> <span class='hs-varid'>g</span><span class='hs-layout'>)</span> <span class='hs-layout'>}</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>FEnv</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>44: </span>
<span class=hs-linenum>45: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>reflect</span> <span class='hs-varid'>in_envF</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>46: </span><span class='hs-definition'>in_envF</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Vname</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Bool</span>
<span class=hs-linenum>47: </span><a class=annot href="#"><span class=annottext>x1:GHC.Types.Int -> x2:BasicsTest1.FEnv -> {VV : GHC.Types.Bool | VV == in_envF x1 x2
&& VV == Set_mem x1 (bindsF x2)}</span><span class='hs-definition'>in_envF</span></a> <a class=annot href="#"><span class=annottext>GHC.Types.Int</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>BasicsTest1.FEnv</span><span class='hs-varid'>g</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>S.member</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == x}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>{v : (Data.Set.Internal.Set GHC.Types.Int) | v == bindsF g}</span><span class='hs-layout'>(</span></a><span class='hs-varid'>bindsF</span> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | v == g}</span><span class='hs-varid'>g</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>48: </span>
<span class=hs-linenum>49: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>reflect</span> <span class='hs-varid'>tv_bound_inF</span> <span class='hs-keyword'>@-}</span> <span class='hs-comment'>-- type variables only</span>
<span class=hs-linenum>50: </span><span class='hs-definition'>tv_bound_inF</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Vname</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Kind</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Bool</span>
<span class=hs-linenum>51: </span><a class=annot href="#"><span class=annottext>x1:GHC.Types.Int -> x2:BasicsTest1.Kind -> x3:BasicsTest1.FEnv -> {VV : GHC.Types.Bool | VV == tv_bound_inF x1 x2 x3}</span><span class='hs-definition'>tv_bound_inF</span></a> <a class=annot href="#"><span class=annottext>GHC.Types.Int</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>BasicsTest1.Kind</span><span class='hs-varid'>k</span></a> <span class='hs-conid'>FEmpty</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | not v
&& v == False}</span><span class='hs-conid'>False</span></a>
<span class=hs-linenum>52: </span><span class='hs-definition'>tv_bound_inF</span> <span class='hs-varid'>a</span> <span class='hs-varid'>k</span> <span class='hs-layout'>(</span><span class='hs-conid'>FCons</span> <span class='hs-varid'>x</span> <span class='hs-varid'>t</span> <span class='hs-varid'>g</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | (v <=> a == x)
&& v == == a x}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a}</span><span class='hs-varid'>a</span></a> <span class='hs-varop'>==</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == x}</span><span class='hs-varid'>x</span></a><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | not v
&& v == False}</span><span class='hs-conid'>False</span></a>
<span class=hs-linenum>53: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:GHC.Types.Int -> x2:BasicsTest1.Kind -> x3:BasicsTest1.FEnv -> {VV : GHC.Types.Bool | VV == tv_bound_inF x1 x2 x3}</span><span class='hs-varid'>tv_bound_inF</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | v == k}</span><span class='hs-varid'>k</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | not (in_envF x v)
&& v == g}</span><span class='hs-varid'>g</span></a>
<span class=hs-linenum>54: </span><span class='hs-definition'>tv_bound_inF</span> <span class='hs-varid'>a</span> <span class='hs-varid'>k</span> <span class='hs-layout'>(</span><span class='hs-conid'>FConsT</span> <span class='hs-varid'>a'</span> <span class='hs-varid'>k'</span> <span class='hs-varid'>g</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | (v <=> a == a')
&& v == == a a'}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a}</span><span class='hs-varid'>a</span></a> <span class='hs-varop'>==</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a'}</span><span class='hs-varid'>a'</span></a><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{v : (GHC.Classes.Eq BasicsTest1.Kind) | v == $fEqKind}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | v == k}</span><span class='hs-varid'>k</span></a> <span class='hs-varop'>==</span> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | v == k'}</span><span class='hs-varid'>k'</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>55: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:GHC.Types.Int -> x2:BasicsTest1.Kind -> x3:BasicsTest1.FEnv -> {VV : GHC.Types.Bool | VV == tv_bound_inF x1 x2 x3}</span><span class='hs-varid'>tv_bound_inF</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | v == k}</span><span class='hs-varid'>k</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | not (in_envF a' v)
&& v == g}</span><span class='hs-varid'>g</span></a>
<span class=hs-linenum>56: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>reflect</span> <span class='hs-varid'>bindsF</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>57: </span><span class='hs-definition'>bindsF</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>S.Set</span> <span class='hs-conid'>Vname</span>
<span class=hs-linenum>58: </span><a class=annot href="#"><span class=annottext>x1:BasicsTest1.FEnv -> {VV : (Data.Set.Internal.Set GHC.Types.Int) | VV == bindsF x1}</span><span class='hs-definition'>bindsF</span></a> <span class='hs-conid'>FEmpty</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : forall a .
{v : (Data.Set.Internal.Set a) | Set_emp v
&& v == empty} | VV == empty}</span><span class='hs-conid'>S.empty</span></a>
<span class=hs-linenum>59: </span><span class='hs-definition'>bindsF</span> <span class='hs-layout'>(</span><span class='hs-conid'>FCons</span> <span class='hs-varid'>x</span> <span class='hs-varid'>t</span> <span class='hs-varid'>g</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{v : (GHC.Classes.Ord GHC.Types.Int) | v == $fOrdInt}</span><span class='hs-conid'>S.union</span></a> <a class=annot href="#"><span class=annottext>{v : (Data.Set.Internal.Set GHC.Types.Int) | v == Set_sng x
&& v == singleton x}</span><span class='hs-layout'>(</span></a><span class='hs-conid'>S.singleton</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == x}</span><span class='hs-varid'>x</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{v : (Data.Set.Internal.Set GHC.Types.Int) | v == bindsF g}</span><span class='hs-layout'>(</span></a><span class='hs-varid'>bindsF</span> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | not (in_envF x v)
&& v == g}</span><span class='hs-varid'>g</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>60: </span><span class='hs-definition'>bindsF</span> <span class='hs-layout'>(</span><span class='hs-conid'>FConsT</span> <span class='hs-varid'>a</span> <span class='hs-varid'>k</span> <span class='hs-varid'>g</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{v : (GHC.Classes.Ord GHC.Types.Int) | v == $fOrdInt}</span><span class='hs-conid'>S.union</span></a> <a class=annot href="#"><span class=annottext>{v : (Data.Set.Internal.Set GHC.Types.Int) | v == Set_sng a
&& v == singleton a}</span><span class='hs-layout'>(</span></a><span class='hs-conid'>S.singleton</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a}</span><span class='hs-varid'>a</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{v : (Data.Set.Internal.Set GHC.Types.Int) | v == bindsF g}</span><span class='hs-layout'>(</span></a><span class='hs-varid'>bindsF</span> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | not (in_envF a v)
&& v == g}</span><span class='hs-varid'>g</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>61: </span>
<span class=hs-linenum>62: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>simple</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>g</span><span class='hs-conop'>:</span><span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{ a:</span><span class='hs-conid'>Vname</span> <span class='hs-keyword'>| in_envF a g }</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{ k:</span><span class='hs-conid'>Kind</span> <span class='hs-keyword'>| tv_bound_inF a k g }</span>
<span class=hs-linenum>63: </span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{ g':</span><span class='hs-conid'>FEnv</span> <span class='hs-keyword'>| not (in_envF a g') }</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>64: </span><span class='hs-definition'>simple</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>FEnv</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Vname</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Kind</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>FEnv</span>
<span class=hs-linenum>65: </span><a class=annot href="#"><span class=annottext>x1:BasicsTest1.FEnv -> x2:{VV : GHC.Types.Int | in_envF VV x1} -> {k : BasicsTest1.Kind | tv_bound_inF x2 k x1} -> {g' : BasicsTest1.FEnv | not (in_envF x2 g')}</span><span class='hs-definition'>simple</span></a> <a class=annot href="#"><span class=annottext>BasicsTest1.FEnv</span><span class='hs-varid'>g</span></a> <a class=annot href="#"><span class=annottext>{VV : GHC.Types.Int | in_envF VV g}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{k : BasicsTest1.Kind | tv_bound_inF a k g}</span><span class='hs-varid'>k</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>case</span> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | v == g}</span><span class='hs-varid'>g</span></a> <span class='hs-keyword'>of</span>
<span class=hs-linenum>66: </span> <span class='hs-layout'>(</span><span class='hs-conid'>FCons</span> <span class='hs-varid'>y</span> <span class='hs-varid'>s</span> <span class='hs-varid'>g'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | (v <=> a == y)
&& v == == a y}</span><span class='hs-layout'>(</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <span class='hs-varop'>==</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == y}</span><span class='hs-varid'>y</span></a> <span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<span class=hs-linenum>67: </span> <span class='hs-layout'>(</span><span class='hs-conid'>False</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>x1:BasicsTest1.FEnv -> x2:{VV : GHC.Types.Int | in_envF VV x1} -> {k : BasicsTest1.Kind | tv_bound_inF x2 k x1} -> {g' : BasicsTest1.FEnv | not (in_envF x2 g')}</span><span class='hs-varid'>simple</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | not (in_envF y v)
&& v == g'}</span><span class='hs-varid'>g'</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | tv_bound_inF a v g
&& v == k}</span><span class='hs-varid'>k</span></a>
<span class=hs-linenum>68: </span> <span class='hs-layout'>(</span><span class='hs-conid'>FConsT</span> <span class='hs-varid'>a'</span> <span class='hs-varid'>k'</span> <span class='hs-varid'>g'</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>case</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Bool | (v <=> a == a')
&& v == == a a'}</span><span class='hs-layout'>(</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <span class='hs-varop'>==</span> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | v == a'}</span><span class='hs-varid'>a'</span></a> <span class='hs-layout'>)</span> <span class='hs-keyword'>of</span>
<span class=hs-linenum>69: </span> <span class='hs-layout'>(</span><span class='hs-conid'>True</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | not (in_envF a' v)
&& v == g'}</span><span class='hs-varid'>g'</span></a>
<span class=hs-linenum>70: </span> <span class='hs-layout'>(</span><span class='hs-conid'>False</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>x1:BasicsTest1.FEnv -> x2:{VV : GHC.Types.Int | in_envF VV x1} -> {k : BasicsTest1.Kind | tv_bound_inF x2 k x1} -> {g' : BasicsTest1.FEnv | not (in_envF x2 g')}</span><span class='hs-varid'>simple</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.FEnv | not (in_envF a' v)
&& v == g'}</span><span class='hs-varid'>g'</span></a> <a class=annot href="#"><span class=annottext>{v : GHC.Types.Int | in_envF v g
&& v == a}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{v : BasicsTest1.Kind | tv_bound_inF a v g
&& v == k}</span><span class='hs-varid'>k</span></a>
</pre>
</body>
</html>