Idris2/tests/codegen/enum/Enum.idr

module Enum

data Foo =
    Foo0
  | Foo1
  | Foo2
  | Foo3
  | Foo4
  | Foo5
  | Foo6
  | Foo7
  | Foo8
  | Foo9
  | Foo10
  | Foo11
  | Foo12
  | Foo13
  | Foo14
  | Foo15
  | Foo16
  | Foo17
  | Foo18
  | Foo19
  | Foo20
  | Foo21
  | Foo22
  | Foo23
  | Foo24
  | Foo25
  | Foo26
  | Foo27
  | Foo28
  | Foo29
  | Foo30
  | Foo31
  | Foo32
  | Foo33
  | Foo34
  | Foo35
  | Foo36
  | Foo37
  | Foo38
  | Foo39
  | Foo40
  | Foo41
  | Foo42
  | Foo43
  | Foo44
  | Foo45
  | Foo46
  | Foo47
  | Foo48
  | Foo49
  | Foo50
  | Foo51
  | Foo52
  | Foo53
  | Foo54
  | Foo55
  | Foo56
  | Foo57
  | Foo58
  | Foo59
  | Foo60
  | Foo61
  | Foo62
  | Foo63
  | Foo64
  | Foo65
  | Foo66
  | Foo67
  | Foo68
  | Foo69
  | Foo70
  | Foo71
  | Foo72
  | Foo73
  | Foo74
  | Foo75
  | Foo76
  | Foo77
  | Foo78
  | Foo79
  | Foo80
  | Foo81
  | Foo82
  | Foo83
  | Foo84
  | Foo85
  | Foo86
  | Foo87
  | Foo88
  | Foo89
  | Foo90
  | Foo91
  | Foo92
  | Foo93
  | Foo94
  | Foo95
  | Foo96
  | Foo97
  | Foo98
  | Foo99
  | Foo100
  | Foo101
  | Foo102
  | Foo103
  | Foo104
  | Foo105
  | Foo106
  | Foo107
  | Foo108
  | Foo109
  | Foo110
  | Foo111
  | Foo112
  | Foo113
  | Foo114
  | Foo115
  | Foo116
  | Foo117
  | Foo118
  | Foo119
  | Foo120

fooToBits8 : Foo -> Bits8
fooToBits8 Foo0 = 0
fooToBits8 Foo1 = 1
fooToBits8 Foo2 = 2
fooToBits8 Foo3 = 3
fooToBits8 Foo4 = 4
fooToBits8 Foo5 = 5
fooToBits8 Foo6 = 6
fooToBits8 Foo7 = 7
fooToBits8 Foo8 = 8
fooToBits8 Foo9 = 9
fooToBits8 Foo10 = 10
fooToBits8 Foo11 = 11
fooToBits8 Foo12 = 12
fooToBits8 Foo13 = 13
fooToBits8 Foo14 = 14
fooToBits8 Foo15 = 15
fooToBits8 Foo16 = 16
fooToBits8 Foo17 = 17
fooToBits8 Foo18 = 18
fooToBits8 Foo19 = 19
fooToBits8 Foo20 = 20
fooToBits8 Foo21 = 21
fooToBits8 Foo22 = 22
fooToBits8 Foo23 = 23
fooToBits8 Foo24 = 24
fooToBits8 Foo25 = 25
fooToBits8 Foo26 = 26
fooToBits8 Foo27 = 27
fooToBits8 Foo28 = 28
fooToBits8 Foo29 = 29
fooToBits8 Foo30 = 30
fooToBits8 Foo31 = 31
fooToBits8 Foo32 = 32
fooToBits8 Foo33 = 33
fooToBits8 Foo34 = 34
fooToBits8 Foo35 = 35
fooToBits8 Foo36 = 36
fooToBits8 Foo37 = 37
fooToBits8 Foo38 = 38
fooToBits8 Foo39 = 39
fooToBits8 Foo40 = 40
fooToBits8 Foo41 = 41
fooToBits8 Foo42 = 42
fooToBits8 Foo43 = 43
fooToBits8 Foo44 = 44
fooToBits8 Foo45 = 45
fooToBits8 Foo46 = 46
fooToBits8 Foo47 = 47
fooToBits8 Foo48 = 48
fooToBits8 Foo49 = 49
fooToBits8 Foo50 = 50
fooToBits8 Foo51 = 51
fooToBits8 Foo52 = 52
fooToBits8 Foo53 = 53
fooToBits8 Foo54 = 54
fooToBits8 Foo55 = 55
fooToBits8 Foo56 = 56
fooToBits8 Foo57 = 57
fooToBits8 Foo58 = 58
fooToBits8 Foo59 = 59
fooToBits8 Foo60 = 60
fooToBits8 Foo61 = 61
fooToBits8 Foo62 = 62
fooToBits8 Foo63 = 63
fooToBits8 Foo64 = 64
fooToBits8 Foo65 = 65
fooToBits8 Foo66 = 66
fooToBits8 Foo67 = 67
fooToBits8 Foo68 = 68
fooToBits8 Foo69 = 69
fooToBits8 Foo70 = 70
fooToBits8 Foo71 = 71
fooToBits8 Foo72 = 72
fooToBits8 Foo73 = 73
fooToBits8 Foo74 = 74
fooToBits8 Foo75 = 75
fooToBits8 Foo76 = 76
fooToBits8 Foo77 = 77
fooToBits8 Foo78 = 78
fooToBits8 Foo79 = 79
fooToBits8 Foo80 = 80
fooToBits8 Foo81 = 81
fooToBits8 Foo82 = 82
fooToBits8 Foo83 = 83
fooToBits8 Foo84 = 84
fooToBits8 Foo85 = 85
fooToBits8 Foo86 = 86
fooToBits8 Foo87 = 87
fooToBits8 Foo88 = 88
fooToBits8 Foo89 = 89
fooToBits8 Foo90 = 90
fooToBits8 Foo91 = 91
fooToBits8 Foo92 = 92
fooToBits8 Foo93 = 93
fooToBits8 Foo94 = 94
fooToBits8 Foo95 = 95
fooToBits8 Foo96 = 96
fooToBits8 Foo97 = 97
fooToBits8 Foo98 = 98
fooToBits8 Foo99 = 99
fooToBits8 Foo100 = 100
fooToBits8 Foo101 = 101
fooToBits8 Foo102 = 102
fooToBits8 Foo103 = 103
fooToBits8 Foo104 = 104
fooToBits8 Foo105 = 105
fooToBits8 Foo106 = 106
fooToBits8 Foo107 = 107
fooToBits8 Foo108 = 108
fooToBits8 Foo109 = 109
fooToBits8 Foo110 = 110
fooToBits8 Foo111 = 111
fooToBits8 Foo112 = 112
fooToBits8 Foo113 = 113
fooToBits8 Foo114 = 114
fooToBits8 Foo115 = 115
fooToBits8 Foo116 = 116
fooToBits8 Foo117 = 117
fooToBits8 Foo118 = 118
fooToBits8 Foo119 = 119
fooToBits8 Foo120 = 120

%inline
Eq Foo where
  x == y = fooToBits8 x == fooToBits8 y

main : IO ()
main = printLn (Foo120 == Foo17)