lue-bird/elm-bounded-nat/18.0.0

NOTE: the latest version is 35.0.0

TypeNats

Express exact natural numbers in a type.

onlyExact1 : Nat (ArgIn min Nat1 ifN_) -> Cake
  • takesOnlyExact1 nat10 is a compile-time error
add2 : Nat (ArgIn min max ifN_) -> Nat (In (Nat2Plus min) (Nat4Plus max))
  • add2 nat2 is of type Nat (In Nat4 (Nat4Plus a_))

about a big limitation

Sadly, while experimenting with type aliases, I discovered that type aliases can only expand so much.

compilingGetsKilled : Nat (N (Nat100Plus Nat93) isA_ isB_)

If a type alias is not fully expanded after ~192 tries,

  • the compilation stops

  • the elm-stuff can corrupt

plus n

type alias Nat100Plus n =
Nat100Plus n

100 + some natural number n.

type alias Nat101Plus n =
Nat101Plus n

101 + some natural number n.

type alias Nat102Plus n =
Nat102Plus n

102 + some natural number n.

type alias Nat103Plus n =
Nat103Plus n

103 + some natural number n.

type alias Nat104Plus n =
Nat104Plus n

104 + some natural number n.

type alias Nat105Plus n =
Nat105Plus n

105 + some natural number n.

type alias Nat106Plus n =
Nat106Plus n

106 + some natural number n.

type alias Nat107Plus n =
Nat107Plus n

107 + some natural number n.

type alias Nat108Plus n =
Nat108Plus n

108 + some natural number n.

type alias Nat109Plus n =
Nat109Plus n

109 + some natural number n.

type alias Nat10Plus n =
Nat10Plus n

10 + some natural number n.

type alias Nat110Plus n =
Nat110Plus n

110 + some natural number n.

type alias Nat111Plus n =
Nat111Plus n

111 + some natural number n.

type alias Nat112Plus n =
Nat112Plus n

112 + some natural number n.

type alias Nat113Plus n =
Nat113Plus n

113 + some natural number n.

type alias Nat114Plus n =
Nat114Plus n

114 + some natural number n.

type alias Nat115Plus n =
Nat115Plus n

115 + some natural number n.

type alias Nat116Plus n =
Nat116Plus n

116 + some natural number n.

type alias Nat117Plus n =
Nat117Plus n

117 + some natural number n.

type alias Nat118Plus n =
Nat118Plus n

118 + some natural number n.

type alias Nat119Plus n =
Nat119Plus n

119 + some natural number n.

type alias Nat11Plus n =
Nat11Plus n

11 + some natural number n.

type alias Nat120Plus n =
Nat120Plus n

120 + some natural number n.

type alias Nat121Plus n =
Nat121Plus n

121 + some natural number n.

type alias Nat122Plus n =
Nat122Plus n

122 + some natural number n.

type alias Nat123Plus n =
Nat123Plus n

123 + some natural number n.

type alias Nat124Plus n =
Nat124Plus n

124 + some natural number n.

type alias Nat125Plus n =
Nat125Plus n

125 + some natural number n.

type alias Nat126Plus n =
Nat126Plus n

126 + some natural number n.

type alias Nat127Plus n =
Nat127Plus n

127 + some natural number n.

type alias Nat128Plus n =
Nat128Plus n

128 + some natural number n.

type alias Nat129Plus n =
Nat129Plus n

129 + some natural number n.

type alias Nat12Plus n =
Nat12Plus n

12 + some natural number n.

type alias Nat130Plus n =
Nat130Plus n

130 + some natural number n.

type alias Nat131Plus n =
Nat131Plus n

131 + some natural number n.

type alias Nat132Plus n =
Nat132Plus n

132 + some natural number n.

type alias Nat133Plus n =
Nat133Plus n

133 + some natural number n.

type alias Nat134Plus n =
Nat134Plus n

134 + some natural number n.

type alias Nat135Plus n =
Nat135Plus n

135 + some natural number n.

type alias Nat136Plus n =
Nat136Plus n

136 + some natural number n.

type alias Nat137Plus n =
Nat137Plus n

137 + some natural number n.

type alias Nat138Plus n =
Nat138Plus n

138 + some natural number n.

type alias Nat139Plus n =
Nat139Plus n

139 + some natural number n.

type alias Nat13Plus n =
Nat13Plus n

13 + some natural number n.

type alias Nat140Plus n =
Nat140Plus n

140 + some natural number n.

type alias Nat141Plus n =
Nat141Plus n

141 + some natural number n.

type alias Nat142Plus n =
Nat142Plus n

142 + some natural number n.

type alias Nat143Plus n =
Nat143Plus n

143 + some natural number n.

type alias Nat144Plus n =
Nat144Plus n

144 + some natural number n.

type alias Nat145Plus n =
Nat145Plus n

145 + some natural number n.

type alias Nat146Plus n =
Nat146Plus n

146 + some natural number n.

type alias Nat147Plus n =
Nat147Plus n

147 + some natural number n.

type alias Nat148Plus n =
Nat148Plus n

148 + some natural number n.

type alias Nat149Plus n =
Nat149Plus n

149 + some natural number n.

type alias Nat14Plus n =
Nat14Plus n

14 + some natural number n.

type alias Nat150Plus n =
Nat150Plus n

150 + some natural number n.

type alias Nat151Plus n =
Nat151Plus n

151 + some natural number n.

type alias Nat152Plus n =
Nat152Plus n

152 + some natural number n.

type alias Nat153Plus n =
Nat153Plus n

153 + some natural number n.

type alias Nat154Plus n =
Nat154Plus n

154 + some natural number n.

type alias Nat155Plus n =
Nat155Plus n

155 + some natural number n.

type alias Nat156Plus n =
Nat156Plus n

156 + some natural number n.

type alias Nat157Plus n =
Nat157Plus n

157 + some natural number n.

type alias Nat158Plus n =
Nat158Plus n

158 + some natural number n.

type alias Nat159Plus n =
Nat159Plus n

159 + some natural number n.

type alias Nat15Plus n =
Nat15Plus n

15 + some natural number n.

type alias Nat160Plus n =
Nat160Plus n

160 + some natural number n.

type alias Nat16Plus n =
Nat16Plus n

16 + some natural number n.

type alias Nat17Plus n =
Nat17Plus n

17 + some natural number n.

type alias Nat18Plus n =
Nat18Plus n

18 + some natural number n.

type alias Nat19Plus n =
Nat19Plus n

19 + some natural number n.

type alias Nat1Plus n =
Nat1Plus n

1 + some natural number n.

type alias Nat20Plus n =
Nat20Plus n

20 + some natural number n.

type alias Nat21Plus n =
Nat21Plus n

21 + some natural number n.

type alias Nat22Plus n =
Nat22Plus n

22 + some natural number n.

type alias Nat23Plus n =
Nat23Plus n

23 + some natural number n.

type alias Nat24Plus n =
Nat24Plus n

24 + some natural number n.

type alias Nat25Plus n =
Nat25Plus n

25 + some natural number n.

type alias Nat26Plus n =
Nat26Plus n

26 + some natural number n.

type alias Nat27Plus n =
Nat27Plus n

27 + some natural number n.

type alias Nat28Plus n =
Nat28Plus n

28 + some natural number n.

type alias Nat29Plus n =
Nat29Plus n

29 + some natural number n.

type alias Nat2Plus n =
Nat2Plus n

2 + some natural number n.

type alias Nat30Plus n =
Nat30Plus n

30 + some natural number n.

type alias Nat31Plus n =
Nat31Plus n

31 + some natural number n.

type alias Nat32Plus n =
Nat32Plus n

32 + some natural number n.

type alias Nat33Plus n =
Nat33Plus n

33 + some natural number n.

type alias Nat34Plus n =
Nat34Plus n

34 + some natural number n.

type alias Nat35Plus n =
Nat35Plus n

35 + some natural number n.

type alias Nat36Plus n =
Nat36Plus n

36 + some natural number n.

type alias Nat37Plus n =
Nat37Plus n

37 + some natural number n.

type alias Nat38Plus n =
Nat38Plus n

38 + some natural number n.

type alias Nat39Plus n =
Nat39Plus n

39 + some natural number n.

type alias Nat3Plus n =
Nat3Plus n

3 + some natural number n.

type alias Nat40Plus n =
Nat40Plus n

40 + some natural number n.

type alias Nat41Plus n =
Nat41Plus n

41 + some natural number n.

type alias Nat42Plus n =
Nat42Plus n

42 + some natural number n.

type alias Nat43Plus n =
Nat43Plus n

43 + some natural number n.

type alias Nat44Plus n =
Nat44Plus n

44 + some natural number n.

type alias Nat45Plus n =
Nat45Plus n

45 + some natural number n.

type alias Nat46Plus n =
Nat46Plus n

46 + some natural number n.

type alias Nat47Plus n =
Nat47Plus n

47 + some natural number n.

type alias Nat48Plus n =
Nat48Plus n

48 + some natural number n.

type alias Nat49Plus n =
Nat49Plus n

49 + some natural number n.

type alias Nat4Plus n =
Nat4Plus n

4 + some natural number n.

type alias Nat50Plus n =
Nat50Plus n

50 + some natural number n.

type alias Nat51Plus n =
Nat51Plus n

51 + some natural number n.

type alias Nat52Plus n =
Nat52Plus n

52 + some natural number n.

type alias Nat53Plus n =
Nat53Plus n

53 + some natural number n.

type alias Nat54Plus n =
Nat54Plus n

54 + some natural number n.

type alias Nat55Plus n =
Nat55Plus n

55 + some natural number n.

type alias Nat56Plus n =
Nat56Plus n

56 + some natural number n.

type alias Nat57Plus n =
Nat57Plus n

57 + some natural number n.

type alias Nat58Plus n =
Nat58Plus n

58 + some natural number n.

type alias Nat59Plus n =
Nat59Plus n

59 + some natural number n.

type alias Nat5Plus n =
Nat5Plus n

5 + some natural number n.

type alias Nat60Plus n =
Nat60Plus n

60 + some natural number n.

type alias Nat61Plus n =
Nat61Plus n

61 + some natural number n.

type alias Nat62Plus n =
Nat62Plus n

62 + some natural number n.

type alias Nat63Plus n =
Nat63Plus n

63 + some natural number n.

type alias Nat64Plus n =
Nat64Plus n

64 + some natural number n.

type alias Nat65Plus n =
Nat65Plus n

65 + some natural number n.

type alias Nat66Plus n =
Nat66Plus n

66 + some natural number n.

type alias Nat67Plus n =
Nat67Plus n

67 + some natural number n.

type alias Nat68Plus n =
Nat68Plus n

68 + some natural number n.

type alias Nat69Plus n =
Nat69Plus n

69 + some natural number n.

type alias Nat6Plus n =
Nat6Plus n

6 + some natural number n.

type alias Nat70Plus n =
Nat70Plus n

70 + some natural number n.

type alias Nat71Plus n =
Nat71Plus n

71 + some natural number n.

type alias Nat72Plus n =
Nat72Plus n

72 + some natural number n.

type alias Nat73Plus n =
Nat73Plus n

73 + some natural number n.

type alias Nat74Plus n =
Nat74Plus n

74 + some natural number n.

type alias Nat75Plus n =
Nat75Plus n

75 + some natural number n.

type alias Nat76Plus n =
Nat76Plus n

76 + some natural number n.

type alias Nat77Plus n =
Nat77Plus n

77 + some natural number n.

type alias Nat78Plus n =
Nat78Plus n

78 + some natural number n.

type alias Nat79Plus n =
Nat79Plus n

79 + some natural number n.

type alias Nat7Plus n =
Nat7Plus n

7 + some natural number n.

type alias Nat80Plus n =
Nat80Plus n

80 + some natural number n.

type alias Nat81Plus n =
Nat81Plus n

81 + some natural number n.

type alias Nat82Plus n =
Nat82Plus n

82 + some natural number n.

type alias Nat83Plus n =
Nat83Plus n

83 + some natural number n.

type alias Nat84Plus n =
Nat84Plus n

84 + some natural number n.

type alias Nat85Plus n =
Nat85Plus n

85 + some natural number n.

type alias Nat86Plus n =
Nat86Plus n

86 + some natural number n.

type alias Nat87Plus n =
Nat87Plus n

87 + some natural number n.

type alias Nat88Plus n =
Nat88Plus n

88 + some natural number n.

type alias Nat89Plus n =
Nat89Plus n

89 + some natural number n.

type alias Nat8Plus n =
Nat8Plus n

8 + some natural number n.

type alias Nat90Plus n =
Nat90Plus n

90 + some natural number n.

type alias Nat91Plus n =
Nat91Plus n

91 + some natural number n.

type alias Nat92Plus n =
Nat92Plus n

92 + some natural number n.

type alias Nat93Plus n =
Nat93Plus n

93 + some natural number n.

type alias Nat94Plus n =
Nat94Plus n

94 + some natural number n.

type alias Nat95Plus n =
Nat95Plus n

95 + some natural number n.

type alias Nat96Plus n =
Nat96Plus n

96 + some natural number n.

type alias Nat97Plus n =
Nat97Plus n

97 + some natural number n.

type alias Nat98Plus n =
Nat98Plus n

98 + some natural number n.

type alias Nat99Plus n =
Nat99Plus n

99 + some natural number n.

type alias Nat9Plus n =
Nat9Plus n

9 + some natural number n.

exact

type alias Nat0 =
Nat0

Exact the natural number 0.

type alias Nat1 =
Nat1

Exact the natural number 1.

type alias Nat10 =
Nat10

Exact the natural number 10.

type alias Nat100 =
Nat100

Exact the natural number 100.

type alias Nat101 =
Nat101

Exact the natural number 101.

type alias Nat102 =
Nat102

Exact the natural number 102.

type alias Nat103 =
Nat103

Exact the natural number 103.

type alias Nat104 =
Nat104

Exact the natural number 104.

type alias Nat105 =
Nat105

Exact the natural number 105.

type alias Nat106 =
Nat106

Exact the natural number 106.

type alias Nat107 =
Nat107

Exact the natural number 107.

type alias Nat108 =
Nat108

Exact the natural number 108.

type alias Nat109 =
Nat109

Exact the natural number 109.

type alias Nat11 =
Nat11

Exact the natural number 11.

type alias Nat110 =
Nat110

Exact the natural number 110.

type alias Nat111 =
Nat111

Exact the natural number 111.

type alias Nat112 =
Nat112

Exact the natural number 112.

type alias Nat113 =
Nat113

Exact the natural number 113.

type alias Nat114 =
Nat114

Exact the natural number 114.

type alias Nat115 =
Nat115

Exact the natural number 115.

type alias Nat116 =
Nat116

Exact the natural number 116.

type alias Nat117 =
Nat117

Exact the natural number 117.

type alias Nat118 =
Nat118

Exact the natural number 118.

type alias Nat119 =
Nat119

Exact the natural number 119.

type alias Nat12 =
Nat12

Exact the natural number 12.

type alias Nat120 =
Nat120

Exact the natural number 120.

type alias Nat121 =
Nat121

Exact the natural number 121.

type alias Nat122 =
Nat122

Exact the natural number 122.

type alias Nat123 =
Nat123

Exact the natural number 123.

type alias Nat124 =
Nat124

Exact the natural number 124.

type alias Nat125 =
Nat125

Exact the natural number 125.

type alias Nat126 =
Nat126

Exact the natural number 126.

type alias Nat127 =
Nat127

Exact the natural number 127.

type alias Nat128 =
Nat128

Exact the natural number 128.

type alias Nat129 =
Nat129

Exact the natural number 129.

type alias Nat13 =
Nat13

Exact the natural number 13.

type alias Nat130 =
Nat130

Exact the natural number 130.

type alias Nat131 =
Nat131

Exact the natural number 131.

type alias Nat132 =
Nat132

Exact the natural number 132.

type alias Nat133 =
Nat133

Exact the natural number 133.

type alias Nat134 =
Nat134

Exact the natural number 134.

type alias Nat135 =
Nat135

Exact the natural number 135.

type alias Nat136 =
Nat136

Exact the natural number 136.

type alias Nat137 =
Nat137

Exact the natural number 137.

type alias Nat138 =
Nat138

Exact the natural number 138.

type alias Nat139 =
Nat139

Exact the natural number 139.

type alias Nat14 =
Nat14

Exact the natural number 14.

type alias Nat140 =
Nat140

Exact the natural number 140.

type alias Nat141 =
Nat141

Exact the natural number 141.

type alias Nat142 =
Nat142

Exact the natural number 142.

type alias Nat143 =
Nat143

Exact the natural number 143.

type alias Nat144 =
Nat144

Exact the natural number 144.

type alias Nat145 =
Nat145

Exact the natural number 145.

type alias Nat146 =
Nat146

Exact the natural number 146.

type alias Nat147 =
Nat147

Exact the natural number 147.

type alias Nat148 =
Nat148

Exact the natural number 148.

type alias Nat149 =
Nat149

Exact the natural number 149.

type alias Nat15 =
Nat15

Exact the natural number 15.

type alias Nat150 =
Nat150

Exact the natural number 150.

type alias Nat151 =
Nat151

Exact the natural number 151.

type alias Nat152 =
Nat152

Exact the natural number 152.

type alias Nat153 =
Nat153

Exact the natural number 153.

type alias Nat154 =
Nat154

Exact the natural number 154.

type alias Nat155 =
Nat155

Exact the natural number 155.

type alias Nat156 =
Nat156

Exact the natural number 156.

type alias Nat157 =
Nat157

Exact the natural number 157.

type alias Nat158 =
Nat158

Exact the natural number 158.

type alias Nat159 =
Nat159

Exact the natural number 159.

type alias Nat16 =
Nat16

Exact the natural number 16.

type alias Nat160 =
Nat160

Exact the natural number 160.

type alias Nat17 =
Nat17

Exact the natural number 17.

type alias Nat18 =
Nat18

Exact the natural number 18.

type alias Nat19 =
Nat19

Exact the natural number 19.

type alias Nat2 =
Nat2

Exact the natural number 2.

type alias Nat20 =
Nat20

Exact the natural number 20.

type alias Nat21 =
Nat21

Exact the natural number 21.

type alias Nat22 =
Nat22

Exact the natural number 22.

type alias Nat23 =
Nat23

Exact the natural number 23.

type alias Nat24 =
Nat24

Exact the natural number 24.

type alias Nat25 =
Nat25

Exact the natural number 25.

type alias Nat26 =
Nat26

Exact the natural number 26.

type alias Nat27 =
Nat27

Exact the natural number 27.

type alias Nat28 =
Nat28

Exact the natural number 28.

type alias Nat29 =
Nat29

Exact the natural number 29.

type alias Nat3 =
Nat3

Exact the natural number 3.

type alias Nat30 =
Nat30

Exact the natural number 30.

type alias Nat31 =
Nat31

Exact the natural number 31.

type alias Nat32 =
Nat32

Exact the natural number 32.

type alias Nat33 =
Nat33

Exact the natural number 33.

type alias Nat34 =
Nat34

Exact the natural number 34.

type alias Nat35 =
Nat35

Exact the natural number 35.

type alias Nat36 =
Nat36

Exact the natural number 36.

type alias Nat37 =
Nat37

Exact the natural number 37.

type alias Nat38 =
Nat38

Exact the natural number 38.

type alias Nat39 =
Nat39

Exact the natural number 39.

type alias Nat4 =
Nat4

Exact the natural number 4.

type alias Nat40 =
Nat40

Exact the natural number 40.

type alias Nat41 =
Nat41

Exact the natural number 41.

type alias Nat42 =
Nat42

Exact the natural number 42.

type alias Nat43 =
Nat43

Exact the natural number 43.

type alias Nat44 =
Nat44

Exact the natural number 44.

type alias Nat45 =
Nat45

Exact the natural number 45.

type alias Nat46 =
Nat46

Exact the natural number 46.

type alias Nat47 =
Nat47

Exact the natural number 47.

type alias Nat48 =
Nat48

Exact the natural number 48.

type alias Nat49 =
Nat49

Exact the natural number 49.

type alias Nat5 =
Nat5

Exact the natural number 5.

type alias Nat50 =
Nat50

Exact the natural number 50.

type alias Nat51 =
Nat51

Exact the natural number 51.

type alias Nat52 =
Nat52

Exact the natural number 52.

type alias Nat53 =
Nat53

Exact the natural number 53.

type alias Nat54 =
Nat54

Exact the natural number 54.

type alias Nat55 =
Nat55

Exact the natural number 55.

type alias Nat56 =
Nat56

Exact the natural number 56.

type alias Nat57 =
Nat57

Exact the natural number 57.

type alias Nat58 =
Nat58

Exact the natural number 58.

type alias Nat59 =
Nat59

Exact the natural number 59.

type alias Nat6 =
Nat6

Exact the natural number 6.

type alias Nat60 =
Nat60

Exact the natural number 60.

type alias Nat61 =
Nat61

Exact the natural number 61.

type alias Nat62 =
Nat62

Exact the natural number 62.

type alias Nat63 =
Nat63

Exact the natural number 63.

type alias Nat64 =
Nat64

Exact the natural number 64.

type alias Nat65 =
Nat65

Exact the natural number 65.

type alias Nat66 =
Nat66

Exact the natural number 66.

type alias Nat67 =
Nat67

Exact the natural number 67.

type alias Nat68 =
Nat68

Exact the natural number 68.

type alias Nat69 =
Nat69

Exact the natural number 69.

type alias Nat7 =
Nat7

Exact the natural number 7.

type alias Nat70 =
Nat70

Exact the natural number 70.

type alias Nat71 =
Nat71

Exact the natural number 71.

type alias Nat72 =
Nat72

Exact the natural number 72.

type alias Nat73 =
Nat73

Exact the natural number 73.

type alias Nat74 =
Nat74

Exact the natural number 74.

type alias Nat75 =
Nat75

Exact the natural number 75.

type alias Nat76 =
Nat76

Exact the natural number 76.

type alias Nat77 =
Nat77

Exact the natural number 77.

type alias Nat78 =
Nat78

Exact the natural number 78.

type alias Nat79 =
Nat79

Exact the natural number 79.

type alias Nat8 =
Nat8

Exact the natural number 8.

type alias Nat80 =
Nat80

Exact the natural number 80.

type alias Nat81 =
Nat81

Exact the natural number 81.

type alias Nat82 =
Nat82

Exact the natural number 82.

type alias Nat83 =
Nat83

Exact the natural number 83.

type alias Nat84 =
Nat84

Exact the natural number 84.

type alias Nat85 =
Nat85

Exact the natural number 85.

type alias Nat86 =
Nat86

Exact the natural number 86.

type alias Nat87 =
Nat87

Exact the natural number 87.

type alias Nat88 =
Nat88

Exact the natural number 88.

type alias Nat89 =
Nat89

Exact the natural number 89.

type alias Nat9 =
Nat9

Exact the natural number 9.

type alias Nat90 =
Nat90

Exact the natural number 90.

type alias Nat91 =
Nat91

Exact the natural number 91.

type alias Nat92 =
Nat92

Exact the natural number 92.

type alias Nat93 =
Nat93

Exact the natural number 93.

type alias Nat94 =
Nat94

Exact the natural number 94.

type alias Nat95 =
Nat95

Exact the natural number 95.

type alias Nat96 =
Nat96

Exact the natural number 96.

type alias Nat97 =
Nat97

Exact the natural number 97.

type alias Nat98 =
Nat98

Exact the natural number 98.

type alias Nat99 =
Nat99

Exact the natural number 99.