Prelude/Eq.ad

Outline



Content


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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148



module Prelude.Eq (
  (====)constant `Prelude.Eq.(====)`
   constant
   type `'a -> 'a -> Prop`
   non-executable,
  EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full(..)class-constant `(=/=)`
class-constant `(===)`
,
  Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates(..)class-constant `(/=)`
class-constant `(==)`

) where

{-# NoImplicitPrelude #-}

import Prelude.Bool
import Prelude.Unit ()
import Prelude.Template

-- | build-in equality, it checks whether there is exactly the same representation of both values
declare non-exec (====)constant `Prelude.Eq.(====)`
   constant
   type `'a -> 'a -> Prop`
   non-executable :: 'atype-variable `'a`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable


-- | sometimes, we do not want absolute identity, but define a congruence relation instead. If we
-- for example define a set-datastructure via distinct lists, (====) will check whether the lists
-- are exactly the same, while (===) checks whether the lists are permutations of each other
class EqP 'atype-variable `'a`
   kind `*` where
  declare non-exec (===)constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable :: 'atype-variable `'a`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
  define non-exec (===)constant `Prelude.Eq.(===)`
   default instance of type-class constant
   type `('a -> 'a -> Prop) -> 'a -> 'a -> Prop`
   non-executable xvariable `x`
   type `'a` yvariable `y`
   type `'a` := notPconstant `Prelude.Bool.notP`
   constant
   type `Prop -> Prop`
   non-executable (xvariable `x`
   type `'a` =/=constant `Prelude.Eq.(=/=)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance yvariable `y`
   type `'a`)

  declare non-exec (=/=)constant `Prelude.Eq.(=/=)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable :: 'atype-variable `'a`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> Proptype `Prelude.Bool.Prop`
   kind `*`
   non-executable
  define non-exec (=/=)constant `Prelude.Eq.(=/=)`
   default instance of type-class constant
   type `('a -> 'a -> Prop) -> 'a -> 'a -> Prop`
   non-executable xvariable `x`
   type `'a` yvariable `y`
   type `'a` := notPconstant `Prelude.Bool.notP`
   constant
   type `Prop -> Prop`
   non-executable (xvariable `x`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance yvariable `y`
   type `'a`)

  property negEqPconstant `Prelude.Eq.negEqP`
   type-class property
   type `'a -> 'a -> Prop`
   non-executable   (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) yvariable `y`
   type `'a`   := (xvariable `x`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance yvariable `y`
   type `'a`) <=/=>constant `Prelude.Bool.(<=/=>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable (xvariable `x`
   type `'a` =/=constant `Prelude.Eq.(=/=)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance yvariable `y`
   type `'a`)
  property reflEqPconstant `Prelude.Eq.reflEqP`
   type-class property
   type `'a -> Prop`
   non-executable  (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`)     := (xvariable `x`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance xvariable `x`
   type `'a`)
  property symEqPconstant `Prelude.Eq.symEqP`
   type-class property
   type `'a -> 'a -> Prop`
   non-executable   (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) yvariable `y`
   type `'a`   := (xvariable `x`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance yvariable `y`
   type `'a`) <=>constant `Prelude.Bool.(<=>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable (yvariable `y`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance xvariable `x`
   type `'a`)
  property transEqPconstant `Prelude.Eq.transEqP`
   type-class property
   type `'a -> 'a -> 'a -> Prop`
   non-executable (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) yvariable `y`
   type `'a` zvariable `z`
   type `'a` := (xvariable `x`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance yvariable `y`
   type `'a`) ==>constant `Prelude.Bool.(==>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable (yvariable `y`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance zvariable `z`
   type `'a`) ==>constant `Prelude.Bool.(==>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable (xvariable `x`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance zvariable `z`
   type `'a`)

  property congEqPconstant `Prelude.Eq.congEqP`
   type-class property
   type `('a -> 'a) -> 'a -> 'a -> Prop`
   non-executable fvariable `f`
   type `'a -> 'a` xvariable `x`
   type `'a` yvariable `y`
   type `'a` := ((((xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance yvariable `y`
   type `'a`) ==>constant `Prelude.Bool.(==>)`
   constant
   type `Prop -> Prop -> Prop`
   non-executable ((fvariable `f`
   type `'a -> 'a` xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   non-executable
   same type-class instance fvariable `f`
   type `'a -> 'a` yvariable `y`
   type `'a`)))

  {-# minimal (===) | (=/=) #-}
end-class

template DeriveInstanceEqPBodyFull (_ :: ClassID, ty :: TypeID, _ :: [String]) := '''
  {{ var constrstemplate-variable `constrs`
   type [ConstID] := tytemplate-variable `ty`
   type TypeID.constructors;
     var clausestemplate-variable `clauses`
   type [String] := [] :: [String];
     foreach var itemplate-variable `i`
   type Nat in constrstemplate-variable `constrs`
   type [ConstID].indices {
       name-scope {
         var (args1template-variable `args1`
   type [String], constr1template-variable `constr1`
   type String) := !ConstWithArgstemplate `Prelude.Template.ConstWithArgs`
   argument-types: (Bool, String, ConstID)
   return-types: ([String], String)
   does not compute text(True, "x", constrstemplate-variable `constrs`
   type [ConstID][itemplate-variable `i`
   type Nat]);
         var (args2template-variable `args2`
   type [String], constr2template-variable `constr2`
   type String) := !ConstWithArgstemplate `Prelude.Template.ConstWithArgs`
   argument-types: (Bool, String, ConstID)
   return-types: ([String], String)
   does not compute text(True, "y", constrstemplate-variable `constrs`
   type [ConstID][itemplate-variable `i`
   type Nat]);
         var cltemplate-variable `cl`
   type String := "(===) " ++ constr1template-variable `constr1`
   type String ++ " " ++ constr2template-variable `constr2`
   type String ++ " := ";
         if (args1template-variable `args1`
   type [String].length > 0) {
           var rhstemplate-variable `rhs`
   type [String] := [] :: [String];
           foreach var xytemplate-variable `xy`
   type (String, String) in zip(args1template-variable `args1`
   type [String], args2template-variable `args2`
   type [String]) {
             rhstemplate-variable `rhs`
   type [String] := insertAtEnd("(" ++ #1(xytemplate-variable `xy`
   type (String, String)) ++ " === " ++ #2(xytemplate-variable `xy`
   type (String, String)) ++ ")", rhstemplate-variable `rhs`
   type [String]);
           }
           cltemplate-variable `cl`
   type String := cltemplate-variable `cl`
   type String ++ !Intercalatetemplate `Prelude.Template.Intercalate`
   argument-types: (String, [String])
   return-type: String
   does not compute text(" /\\ ", rhstemplate-variable `rhs`
   type [String]);
         } else {
           cltemplate-variable `cl`
   type String := cltemplate-variable `cl`
   type String ++ "true"
         }
         clausestemplate-variable `clauses`
   type [String] := insertAtEnd(cltemplate-variable `cl`
   type String, clausestemplate-variable `clauses`
   type [String]);
       }
     }
     if (constrstemplate-variable `constrs`
   type [ConstID].length > 1) {
       clausestemplate-variable `clauses`
   type [String] := insertAtEnd("(===) _ _ := false", clausestemplate-variable `clauses`
   type [String]);
     }
     var recDecltemplate-variable `recDecl`
   type String, indentRectemplate-variable `indentRec`
   type String := "";
     if (tytemplate-variable `ty`
   type TypeID.isRec) { recDecltemplate-variable `recDecl`
   type String := "rec "; indentRectemplate-variable `indentRec`
   type String := "    "; }
  }}
{{= "define non-exec " ++ recDecltemplate-variable `recDecl`
   type String ++ !Intercalatetemplate `Prelude.Template.Intercalate`
   argument-types: (String, [String])
   return-type: String
   does not compute text("\n              "++indentRectemplate-variable `indentRec`
   type String++"| ", clausestemplate-variable `clauses`
   type [String]) =}}
'''

register-derive-template EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full DeriveInstanceEqPBodyFulltemplate `Prelude.Eq.DeriveInstanceEqPBodyFull`
   argument-types: (ClassID, TypeID, [String])
   return-type: - as "full"

template DeriveInstanceEqPBodyEq (_ :: ClassID, ty :: TypeID, _ :: [String]) := '''
define non-exec (===) x y := bool2prop (x == y)
'''

register-derive-template EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full DeriveInstanceEqPBodyEqtemplate `Prelude.Eq.DeriveInstanceEqPBodyEq`
   argument-types: (ClassID, TypeID, [String])
   return-type: - - as "eq"

template DeriveInstanceEqPBody (cl :: ClassID, ty :: TypeID, args :: [String]) := '''
{{% if (argstemplate-variable `args`
   type [String].length == 0) %}}
{{! DeriveInstanceEqPBodyEqtemplate `Prelude.Eq.DeriveInstanceEqPBodyEq`
   argument-types: (ClassID, TypeID, [String])
   return-type: -(cltemplate-variable `cl`
   type ClassID, tytemplate-variable `ty`
   type TypeID, argstemplate-variable `args`
   type [String]) !}}
{{% else %}}
{{! DeriveInstanceEqPBodyFulltemplate `Prelude.Eq.DeriveInstanceEqPBodyFull`
   argument-types: (ClassID, TypeID, [String])
   return-type: -(cltemplate-variable `cl`
   type ClassID, tytemplate-variable `ty`
   type TypeID, argstemplate-variable `args`
   type [String]) !}}
{{% end-if %}}
'''

register-derive-template EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full DeriveInstanceEqPBodytemplate `Prelude.Eq.DeriveInstanceEqPBody`
   argument-types: (ClassID, TypeID, [String])
   return-type: -

instance EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full 'btype-variable `'b`
   kind `*` => EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full ('atype-variable `'a`
   kind `*` -> 'btype-variable `'b`
   kind `*`) where
  define non-exec (===)constant `Prelude.Eq.(===)`
   constant of type-class instance `EqP 'b => EqP ('a -> 'b)`
   type `('a -> 'b) -> ('a -> 'b) -> Prop`
   non-executable f1variable `f1`
   type `'a -> 'b` f2variable `f2`
   type `'a -> 'b` := forallP avariable `a`
   type `'a`. f1variable `f1`
   type `'a -> 'b` avariable `a`
   type `'a` ===constant `Prelude.Eq.(===)`
   constant of type-class `EqP`
   type `'a -> 'a -> Prop`
   type in context `'b -> 'b -> Prop`
   non-executable
   type-class instance from context f2variable `f2`
   type `'a -> 'b` avariable `a`
   type `'a`
end-instance

-- | (===) is not computable. An example is an equality check for functions, which might not be
-- computable. For computing computability (==) is provided.
class EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full 'atype-variable `'a`
   kind `*` => Eq 'atype-variable `'a`
   kind `*` where
  declare (==)constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable :: 'atype-variable `'a`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable
  define (==)constant `Prelude.Eq.(==)`
   default instance of type-class constant
   type `('a -> 'a -> Bool) -> 'a -> 'a -> Bool`
   executable xvariable `x`
   type `'a` yvariable `y`
   type `'a` := notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable (xvariable `x`
   type `'a` /=constant `Prelude.Eq.(/=)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance yvariable `y`
   type `'a`)

  declare (/=)constant `Prelude.Eq.(/=)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable :: 'atype-variable `'a`
   kind `*` -> 'atype-variable `'a`
   kind `*` -> Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable
  define (/=)constant `Prelude.Eq.(/=)`
   default instance of type-class constant
   type `('a -> 'a -> Bool) -> 'a -> 'a -> Bool`
   executable xvariable `x`
   type `'a` yvariable `y`
   type `'a` := notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable (xvariable `x`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance yvariable `y`
   type `'a`)

  test negEqconstant `Prelude.Eq.negEq`
   type-class test
   type `'a -> 'a -> Bool`
   executable   (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) yvariable `y`
   type `'a`   := (xvariable `x`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance yvariable `y`
   type `'a`) <->constant `Prelude.Bool.(<->)`
   constant
   type `Bool -> Bool -> Bool`
   executable (notconstant `Prelude.Bool.not`
   constant
   type `Bool -> Bool`
   executable (xvariable `x`
   type `'a` /=constant `Prelude.Eq.(/=)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance yvariable `y`
   type `'a`))
  test reflEqconstant `Prelude.Eq.reflEq`
   type-class test
   type `'a -> Bool`
   executable  (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`)     := (xvariable `x`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance xvariable `x`
   type `'a`)
  test symEqconstant `Prelude.Eq.symEq`
   type-class test
   type `'a -> 'a -> Bool`
   executable   (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) yvariable `y`
   type `'a`   := (xvariable `x`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance yvariable `y`
   type `'a`) <->constant `Prelude.Bool.(<->)`
   constant
   type `Bool -> Bool -> Bool`
   executable (yvariable `y`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance xvariable `x`
   type `'a`)
  test transEqconstant `Prelude.Eq.transEq`
   type-class test
   type `'a -> 'a -> 'a -> Bool`
   executable (xvariable `x`
   type `'a` :: 'atype-variable `'a`
   kind `*`) yvariable `y`
   type `'a` zvariable `z`
   type `'a` := (xvariable `x`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance yvariable `y`
   type `'a`) -->constant `Prelude.Bool.(-->)`
   constant
   type `Bool -> Bool -> Bool`
   executable (yvariable `y`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance zvariable `z`
   type `'a`) -->constant `Prelude.Bool.(-->)`
   constant
   type `Bool -> Bool -> Bool`
   executable (xvariable `x`
   type `'a` ==constant `Prelude.Eq.(==)`
   constant of type-class `Eq`
   type `'a -> 'a -> Bool`
   executable
   same type-class instance zvariable `z`
   type `'a`)

  -- property eqProp x y := (((x :: 'a) == y) === True) <=> (x === y)
  {-# minimal (==) | (/=) #-}
end-class

template DeriveInstanceEqBody (_ :: ClassID, ty :: TypeID, _ :: [String]) := '''
  {{ var constrstemplate-variable `constrs`
   type [ConstID] := tytemplate-variable `ty`
   type TypeID.constructors;
     var clausestemplate-variable `clauses`
   type [String] := [] :: [String];
     foreach var itemplate-variable `i`
   type Nat in constrstemplate-variable `constrs`
   type [ConstID].indices {
       name-scope {
         var (args1template-variable `args1`
   type [String], constr1template-variable `constr1`
   type String) := !ConstWithArgstemplate `Prelude.Template.ConstWithArgs`
   argument-types: (Bool, String, ConstID)
   return-types: ([String], String)
   does not compute text(True, "x", constrstemplate-variable `constrs`
   type [ConstID][itemplate-variable `i`
   type Nat]);
         var (args2template-variable `args2`
   type [String], constr2template-variable `constr2`
   type String) := !ConstWithArgstemplate `Prelude.Template.ConstWithArgs`
   argument-types: (Bool, String, ConstID)
   return-types: ([String], String)
   does not compute text(True, "y", constrstemplate-variable `constrs`
   type [ConstID][itemplate-variable `i`
   type Nat]);
         var cltemplate-variable `cl`
   type String := "(==) " ++ constr1template-variable `constr1`
   type String ++ " " ++ constr2template-variable `constr2`
   type String ++ " := ";
         if (args1template-variable `args1`
   type [String].length > 0) {
           var rhstemplate-variable `rhs`
   type [String] := [] :: [String];
           foreach var xytemplate-variable `xy`
   type (String, String) in zip(args1template-variable `args1`
   type [String], args2template-variable `args2`
   type [String]) {
             rhstemplate-variable `rhs`
   type [String] := insertAtEnd("(" ++ #1(xytemplate-variable `xy`
   type (String, String)) ++ " == " ++ #2(xytemplate-variable `xy`
   type (String, String)) ++ ")", rhstemplate-variable `rhs`
   type [String]);
           }
           cltemplate-variable `cl`
   type String := cltemplate-variable `cl`
   type String ++ !Intercalatetemplate `Prelude.Template.Intercalate`
   argument-types: (String, [String])
   return-type: String
   does not compute text(" && ", rhstemplate-variable `rhs`
   type [String]);
         } else {
           cltemplate-variable `cl`
   type String := cltemplate-variable `cl`
   type String ++ "True"
         }
         clausestemplate-variable `clauses`
   type [String] := insertAtEnd(cltemplate-variable `cl`
   type String, clausestemplate-variable `clauses`
   type [String]);
       }
     }
     if (constrstemplate-variable `constrs`
   type [ConstID].length > 1) {
       clausestemplate-variable `clauses`
   type [String] := insertAtEnd("(==) _ _ := False", clausestemplate-variable `clauses`
   type [String]);
     }
     var recDecltemplate-variable `recDecl`
   type String, indentRectemplate-variable `indentRec`
   type String := "";
     if (tytemplate-variable `ty`
   type TypeID.isRec) { recDecltemplate-variable `recDecl`
   type String := "rec "; indentRectemplate-variable `indentRec`
   type String := "    "; }
  }}
{{= "define " ++ recDecltemplate-variable `recDecl`
   type String ++ !Intercalatetemplate `Prelude.Template.Intercalate`
   argument-types: (String, [String])
   return-type: String
   does not compute text("\n     "++indentRectemplate-variable `indentRec`
   type String++"| ", clausestemplate-variable `clauses`
   type [String]) =}}
'''

register-derive-template Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates DeriveInstanceEqBodytemplate `Prelude.Eq.DeriveInstanceEqBody`
   argument-types: (ClassID, TypeID, [String])
   return-type: -


instance Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates () where
  define (==)constant `Prelude.Eq.(==)`
   constant of type-class instance `Eq ()`
   type `() -> () -> Bool`
   executable _ _ := Trueconstant `Prelude.Bool.True`
   constructor of datatype `Bool`
   type `Bool`
   executable
end-instance

instance EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full () where
  define non-exec (===)constant `Prelude.Eq.(===)`
   constant of type-class instance `EqP ()`
   type `() -> () -> Prop`
   non-executable _ _ := trueconstant `Prelude.Bool.true`
   constant
   type `Prop`
   non-executable
end-instance

derive Booldatatype `Prelude.Bool.Bool`
   kind `*`
   executable instances (EqPtype-class `Prelude.Eq.EqP`
   arguments: ('a :: *)
   has default derive templates
   derive-template labels
     - eq (only deriving)
     - full
generated code:

instance EqP Bool where
  define non-exec (===) x y := bool2prop (x == y)
end-instance
, Eqtype-class `Prelude.Eq.Eq`
   arguments: ('a :: *)
   super-class constraints:
     - Prelude.Eq.EqP 'a
   has default derive templates
generated code:

instance Eq Bool where
  define (==) False False := True
       | (==) True True := True
       | (==) _ _ := False
end-instance
)

end-moduleend of module Prelude.Eq