0ffb7b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix violations of parametricity

0ffb7b6Benjamin Saunders14 years ago

lib/Prelude/Bits.idr+133−131

compare with master

unifiedsplit

@@ -10,16 +10,18 @@ log2ceil n = let x = log2 n in

10 then x+1

11 else x

13−nextBits : Nat -> Type

13+log2Bytes : Nat -> Nat

14−nextBits x with (log2ceil x)

14+log2Bytes bits = (log2ceil (bits `div` 8))

15− | (S (S (S (S (S (S _)))))) = Bits64

15+

16− | (S (S (S (S (S O))))) = Bits32

16+machineTy : Nat -> Type

17− | (S (S (S (S O)))) = Bits16

18− | _ = Bits8

17+machineTy O = Bits8

18+machineTy (S O) = Bits16

19+machineTy (S (S O)) = Bits32

20+machineTy (S (S (S _))) = Bits64

20public

22public

21data Bits : Nat -> Type where

23data Bits : Nat -> Type where

22− MkBits : {n : Nat} -> nextBits n -> Bits n

24+ MkBits : {n : Nat} -> machineTy (log2Bytes n) -> Bits n

24pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

26pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8

25pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad

27pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad

@@ -69,16 +71,16 @@ pow x y = if y > 0

69 else 1

71 else 1

71%assert_total

73%assert_total

72−intToBits' : {n : Nat} -> Int -> nextBits n

74+intToBits' : {n : Nat} -> Int -> machineTy (log2Bytes n)

73−intToBits' {n=n} x with (nextBits n)

75+intToBits' {n=n} x with (log2Bytes n)

74− | Bits8 = let pad = (prim__intToB8 (cast (8-n))) in

76+ | O = let pad = (prim__intToB8 (cast (8-n))) in

75− prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad

77+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad

76− | Bits16 = let pad = (prim__intToB16 (cast (16-n))) in

78+ | S O = let pad = (prim__intToB16 (cast (16-n))) in

77− prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad

79+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad

78− | Bits32 = let pad = (prim__intToB32 (cast (32-n))) in

80+ | S (S O) = let pad = (prim__intToB32 (cast (32-n))) in

79− prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad

81+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad

80− | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in

82+ | S (S (S _)) = let pad = (prim__intToB64 (cast (64-n))) in

81− prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad

83+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad

83public

85public

84intToBits : {n : Nat} -> Int -> Bits n

86intToBits : {n : Nat} -> Int -> Bits n

@@ -87,215 +89,215 @@ intToBits n = MkBits (intToBits' n)

87instance Cast Int (Bits n) where

89instance Cast Int (Bits n) where

88 cast = intToBits

90 cast = intToBits

90−unsafeBitsToInt' : {n : Nat} -> nextBits n -> Int

92+unsafeBitsToInt' : {n : Nat} -> machineTy (log2Bytes n) -> Int

91−unsafeBitsToInt' {n=n} x with (nextBits n)

93+unsafeBitsToInt' {n=n} x with (log2Bytes n)

92− | Bits8 = prim__B32ToInt (prim__zextB8_32 x)

94+ | O = prim__B32ToInt (prim__zextB8_32 x)

93− | Bits16 = prim__B32ToInt (prim__zextB16_32 x)

95+ | S O = prim__B32ToInt (prim__zextB16_32 x)

94− | Bits32 = prim__B32ToInt x

96+ | S (S O) = prim__B32ToInt x

95− | Bits64 = prim__B32ToInt (prim__truncB64_32 x)

97+ | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)

97public

99public

98unsafeBitsToInt : Bits n -> Int

100unsafeBitsToInt : Bits n -> Int

99unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x

101unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x

100

102

101−bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n

103+bitsShl' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

102−bitsShl' {n=n} x c with (nextBits n)

104+bitsShl' {n=n} x c with (log2Bytes n)

103− | Bits8 = pad8' n prim__shlB8 x c

105+ | O = pad8' n prim__shlB8 x c

104− | Bits16 = pad16' n prim__shlB16 x c

106+ | S O = pad16' n prim__shlB16 x c

105− | Bits32 = pad32' n prim__shlB32 x c

107+ | S (S O) = pad32' n prim__shlB32 x c

106− | Bits64 = pad64' n prim__shlB64 x c

108+ | S (S (S _)) = pad64' n prim__shlB64 x c

107

109

108public

110public

109bitsShl : Bits n -> Bits n -> Bits n

111bitsShl : Bits n -> Bits n -> Bits n

110bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)

112bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)

111

113

112−bitsLShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n

114+bitsLShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

113−bitsLShr' {n=n} x c with (nextBits n)

115+bitsLShr' {n=n} x c with (log2Bytes n)

114− | Bits8 = prim__lshrB8 x c

116+ | O = prim__lshrB8 x c

115− | Bits16 = prim__lshrB16 x c

117+ | S O = prim__lshrB16 x c

116− | Bits32 = prim__lshrB32 x c

118+ | S (S O) = prim__lshrB32 x c

117− | Bits64 = prim__lshrB64 x c

119+ | S (S (S _)) = prim__lshrB64 x c

118

120

119public

121public

120bitsLShr : Bits n -> Bits n -> Bits n

122bitsLShr : Bits n -> Bits n -> Bits n

121bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)

123bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)

122

124

123−bitsAShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n

125+bitsAShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

124−bitsAShr' {n=n} x c with (nextBits n)

126+bitsAShr' {n=n} x c with (log2Bytes n)

125− | Bits8 = prim__ashrB8 x c

127+ | O = prim__ashrB8 x c

126− | Bits16 = prim__ashrB16 x c

128+ | S O = prim__ashrB16 x c

127− | Bits32 = prim__ashrB32 x c

129+ | S (S O) = prim__ashrB32 x c

128− | Bits64 = prim__ashrB64 x c

130+ | S (S (S _)) = prim__ashrB64 x c

129

131

130public

132public

131bitsAShr : Bits n -> Bits n -> Bits n

133bitsAShr : Bits n -> Bits n -> Bits n

132bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)

134bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)

133

135

134−bitsAnd' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n

136+bitsAnd' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

135−bitsAnd' {n=n} x y with (nextBits n)

137+bitsAnd' {n=n} x y with (log2Bytes n)

136− | Bits8 = prim__andB8 x y

138+ | O = prim__andB8 x y

137− | Bits16 = prim__andB16 x y

139+ | S O = prim__andB16 x y

138− | Bits32 = prim__andB32 x y

140+ | S (S O) = prim__andB32 x y

139− | Bits64 = prim__andB64 x y

141+ | S (S (S _)) = prim__andB64 x y

140

142

141public

143public

142bitsAnd : Bits n -> Bits n -> Bits n

144bitsAnd : Bits n -> Bits n -> Bits n

143bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)

145bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)

144

146

145−bitsOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n

147+bitsOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

146−bitsOr' {n=n} x y with (nextBits n)

148+bitsOr' {n=n} x y with (log2Bytes n)

147− | Bits8 = prim__orB8 x y

149+ | O = prim__orB8 x y

148− | Bits16 = prim__orB16 x y

150+ | S O = prim__orB16 x y

149− | Bits32 = prim__orB32 x y

151+ | S (S O) = prim__orB32 x y

150− | Bits64 = prim__orB64 x y

152+ | S (S (S _)) = prim__orB64 x y

151

153

152public

154public

153bitsOr : Bits n -> Bits n -> Bits n

155bitsOr : Bits n -> Bits n -> Bits n

154bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)

156bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)

155

157

156−bitsXOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n

158+bitsXOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

157−bitsXOr' {n=n} x y with (nextBits n)

159+bitsXOr' {n=n} x y with (log2Bytes n)

158− | Bits8 = prim__xorB8 x y

160+ | O = prim__xorB8 x y

159− | Bits16 = prim__xorB16 x y

161+ | S O = prim__xorB16 x y

160− | Bits32 = prim__xorB32 x y

162+ | S (S O) = prim__xorB32 x y

161− | Bits64 = prim__xorB64 x y

163+ | S (S (S _)) = prim__xorB64 x y

162

164

163public

165public

164bitsXOr : Bits n -> Bits n -> Bits n

166bitsXOr : Bits n -> Bits n -> Bits n

165bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)

167bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)

166

168

167−bitsAdd' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

169+bitsAdd' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

168−bitsAdd' {n=n} x y with (nextBits n)

170+bitsAdd' {n=n} x y with (log2Bytes n)

169− | Bits8 = pad8 n prim__addB8 x y

171+ | O = pad8 n prim__addB8 x y

170− | Bits16 = pad16 n prim__addB16 x y

172+ | S O = pad16 n prim__addB16 x y

171− | Bits32 = pad32 n prim__addB32 x y

173+ | S (S O) = pad32 n prim__addB32 x y

172− | Bits64 = pad64 n prim__addB64 x y

174+ | S (S (S _)) = pad64 n prim__addB64 x y

173

175

174public

176public

175bitsAdd : Bits n -> Bits n -> Bits n

177bitsAdd : Bits n -> Bits n -> Bits n

176bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)

178bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)

177

179

178−bitsSub' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

180+bitsSub' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

179−bitsSub' {n=n} x y with (nextBits n)

181+bitsSub' {n=n} x y with (log2Bytes n)

180− | Bits8 = pad8 n prim__subB8 x y

182+ | O = pad8 n prim__subB8 x y

181− | Bits16 = pad16 n prim__subB16 x y

183+ | S O = pad16 n prim__subB16 x y

182− | Bits32 = pad32 n prim__subB32 x y

184+ | S (S O) = pad32 n prim__subB32 x y

183− | Bits64 = pad64 n prim__subB64 x y

185+ | S (S (S _)) = pad64 n prim__subB64 x y

184

186

185public

187public

186bitsSub : Bits n -> Bits n -> Bits n

188bitsSub : Bits n -> Bits n -> Bits n

187bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)

189bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)

188

190

189−bitsMul' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

191+bitsMul' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

190−bitsMul' {n=n} x y with (nextBits n)

192+bitsMul' {n=n} x y with (log2Bytes n)

191− | Bits8 = pad8 n prim__mulB8 x y

193+ | O = pad8 n prim__mulB8 x y

192− | Bits16 = pad16 n prim__mulB16 x y

194+ | S O = pad16 n prim__mulB16 x y

193− | Bits32 = pad32 n prim__mulB32 x y

195+ | S (S O) = pad32 n prim__mulB32 x y

194− | Bits64 = pad64 n prim__mulB64 x y

196+ | S (S (S _)) = pad64 n prim__mulB64 x y

195

197

196public

198public

197bitsMul : Bits n -> Bits n -> Bits n

199bitsMul : Bits n -> Bits n -> Bits n

198bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)

200bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)

199

201

200partial

202partial

201−bitsSDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

203+bitsSDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

202−bitsSDiv' {n=n} x y with (nextBits n)

204+bitsSDiv' {n=n} x y with (log2Bytes n)

203− | Bits8 = prim__sdivB8 x y

205+ | O = prim__sdivB8 x y

204− | Bits16 = prim__sdivB16 x y

206+ | S O = prim__sdivB16 x y

205− | Bits32 = prim__sdivB32 x y

207+ | S (S O) = prim__sdivB32 x y

206− | Bits64 = prim__sdivB64 x y

208+ | S (S (S _)) = prim__sdivB64 x y

207

209

208public partial

210public partial

209bitsSDiv : Bits n -> Bits n -> Bits n

211bitsSDiv : Bits n -> Bits n -> Bits n

210bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)

212bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)

211

213

212partial

214partial

213−bitsUDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

215+bitsUDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

214−bitsUDiv' {n=n} x y with (nextBits n)

216+bitsUDiv' {n=n} x y with (log2Bytes n)

215− | Bits8 = prim__udivB8 x y

217+ | O = prim__udivB8 x y

216− | Bits16 = prim__udivB16 x y

218+ | S O = prim__udivB16 x y

217− | Bits32 = prim__udivB32 x y

219+ | S (S O) = prim__udivB32 x y

218− | Bits64 = prim__udivB64 x y

220+ | S (S (S _)) = prim__udivB64 x y

219

221

220public partial

222public partial

221bitsUDiv : Bits n -> Bits n -> Bits n

223bitsUDiv : Bits n -> Bits n -> Bits n

222bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)

224bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)

223

225

224partial

226partial

225−bitsSRem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

227+bitsSRem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

226−bitsSRem' {n=n} x y with (nextBits n)

228+bitsSRem' {n=n} x y with (log2Bytes n)

227− | Bits8 = prim__sremB8 x y

229+ | O = prim__sremB8 x y

228− | Bits16 = prim__sremB16 x y

230+ | S O = prim__sremB16 x y

229− | Bits32 = prim__sremB32 x y

231+ | S (S O) = prim__sremB32 x y

230− | Bits64 = prim__sremB64 x y

232+ | S (S (S _)) = prim__sremB64 x y

231

233

232public partial

234public partial

233bitsSRem : Bits n -> Bits n -> Bits n

235bitsSRem : Bits n -> Bits n -> Bits n

234bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)

236bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)

235

237

236partial

238partial

237−bitsURem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n

239+bitsURem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)

238−bitsURem' {n=n} x y with (nextBits n)

240+bitsURem' {n=n} x y with (log2Bytes n)

239− | Bits8 = prim__uremB8 x y

241+ | O = prim__uremB8 x y

240− | Bits16 = prim__uremB16 x y

242+ | S O = prim__uremB16 x y

241− | Bits32 = prim__uremB32 x y

243+ | S (S O) = prim__uremB32 x y

242− | Bits64 = prim__uremB64 x y

244+ | S (S (S _)) = prim__uremB64 x y

243

245

244public partial

246public partial

245bitsURem : Bits n -> Bits n -> Bits n

247bitsURem : Bits n -> Bits n -> Bits n

246bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)

248bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)

247

249

248-- TODO: Proofy comparisons via postulates

250-- TODO: Proofy comparisons via postulates

249−bitsLt' : (x : nextBits n) -> (y : nextBits n) -> Int

251+bitsLt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int

250−bitsLt' {n=n} x y with (nextBits n)

252+bitsLt' {n=n} x y with (log2Bytes n)

251− | Bits8 = prim__ltB8 x y

253+ | O = prim__ltB8 x y

252− | Bits16 = prim__ltB16 x y

254+ | S O = prim__ltB16 x y

253− | Bits32 = prim__ltB32 x y

255+ | S (S O) = prim__ltB32 x y

254− | Bits64 = prim__ltB64 x y

256+ | S (S (S _)) = prim__ltB64 x y

255

257

256public

258public

257bitsLt : (x : Bits n) -> (y : Bits n) -> Bool

259bitsLt : (x : Bits n) -> (y : Bits n) -> Bool

258bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0

260bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0

259

261

260−bitsLte' : (x : nextBits n) -> (y : nextBits n) -> Int

262+bitsLte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int

261−bitsLte' {n=n} x y with (nextBits n)

263+bitsLte' {n=n} x y with (log2Bytes n)

262− | Bits8 = prim__lteB8 x y

264+ | O = prim__lteB8 x y

263− | Bits16 = prim__lteB16 x y

265+ | S O = prim__lteB16 x y

264− | Bits32 = prim__lteB32 x y

266+ | S (S O) = prim__lteB32 x y

265− | Bits64 = prim__lteB64 x y

267+ | S (S (S _)) = prim__lteB64 x y

266

268

267public

269public

268bitsLte : (x : Bits n) -> (y : Bits n) -> Bool

270bitsLte : (x : Bits n) -> (y : Bits n) -> Bool

269bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0

271bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0

270

272

271−bitsEq' : (x : nextBits n) -> (y : nextBits n) -> Int

273+bitsEq' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int

272−bitsEq' {n=n} x y with (nextBits n)

274+bitsEq' {n=n} x y with (log2Bytes n)

273− | Bits8 = prim__eqB8 x y

275+ | O = prim__eqB8 x y

274− | Bits16 = prim__eqB16 x y

276+ | S O = prim__eqB16 x y

275− | Bits32 = prim__eqB32 x y

277+ | S (S O) = prim__eqB32 x y

276− | Bits64 = prim__eqB64 x y

278+ | S (S (S _)) = prim__eqB64 x y

277

279

278public

280public

279bitsEq : (x : Bits n) -> (y : Bits n) -> Bool

281bitsEq : (x : Bits n) -> (y : Bits n) -> Bool

280bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0

282bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0

281

283

282−bitsGte' : (x : nextBits n) -> (y : nextBits n) -> Int

284+bitsGte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int

283−bitsGte' {n=n} x y with (nextBits n)

285+bitsGte' {n=n} x y with (log2Bytes n)

284− | Bits8 = prim__gteB8 x y

286+ | O = prim__gteB8 x y

285− | Bits16 = prim__gteB16 x y

287+ | S O = prim__gteB16 x y

286− | Bits32 = prim__gteB32 x y

288+ | S (S O) = prim__gteB32 x y

287− | Bits64 = prim__gteB64 x y

289+ | S (S (S _)) = prim__gteB64 x y

288

290

289public

291public

290bitsGte : (x : Bits n) -> (y : Bits n) -> Bool

292bitsGte : (x : Bits n) -> (y : Bits n) -> Bool

291bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0

293bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0

292

294

293−bitsGt' : (x : nextBits n) -> (y : nextBits n) -> Int

295+bitsGt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int

294−bitsGt' {n=n} x y with (nextBits n)

296+bitsGt' {n=n} x y with (log2Bytes n)

295− | Bits8 = prim__gtB8 x y

297+ | O = prim__gtB8 x y

296− | Bits16 = prim__gtB16 x y

298+ | S O = prim__gtB16 x y

297− | Bits32 = prim__gtB32 x y

299+ | S (S O) = prim__gtB32 x y

298− | Bits64 = prim__gtB64 x y

300+ | S (S (S _)) = prim__gtB64 x y

299

301

300public

302public

301bitsGt : (x : Bits n) -> (y : Bits n) -> Bool

303bitsGt : (x : Bits n) -> (y : Bits n) -> Bool