// TMD: I am using this issue for a range of regressions or short-comings with the new type checker.
// Let me know if you'd like separate github issue numbers.

// Want: exact width values is nice (width x == const ==> width x >= const)
// Issue: Cryptol wants 'width x >= const'
// width_eq_geq : {n} (32 == width n, n >= 1, 32 >= width n, fin n) => [n]Bit
width_eq_geq : {n} (32 == width n, n >= 1) => [n]Bit
width_eq_geq = [True | _ <- [1..n] : [_][32] ]

// Want: const >= width (x+1) ==> const > width x
// or any monotonic function, not just addition.
//
// Also Want: const >= width n     ==> fin n
//
// Issue: Cryptol wants '64 >= width n' and 'fin n'
// can_not_width : {n} (64 >= width (8*(n+1)), 64 >= width n, fin n) => [64]
can_not_width : {n} (64 >= width (8*(n+1))) => [64]
can_not_width = zero # (`n : [width n])

// Want: Honestly, I don't know what's going on here.  It seems to relate to some of our regressions though.
// Tell me if there should be another ticket - probably one that already exists. -TMD
// Issue: Cryptol 2.3 wants 'n == 4 + (?a3 - n % 4)'
take_knows_no_bounds : {n} (fin n, n >= 4) => [n][8] -> [4 - (n%4)][8]
take_knows_no_bounds ns = foo
 where
 foo = take `{4 - (n%4)} ns