def fl_len

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbytes.bend:143

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

143# any other length parses to None
144def fl_len(+k: Nat, xs: List<&2, Nat>, +h: {Nat.is_eq(C.length(Nat, xs), k) == False{} : Bool}) -> {SF.from_le(k, xs) == None{} : Maybe<&2, Nat>}:
145  match k xs:
146    case 0n Nil{}:
147      Empty.absurd({SF.from_le(0n, Nil{}) == None{} : Maybe<&2, Nat>}, L.true_false(h))
148    case 0n Con{+x, t}:
149      {==}
150    case 1n+ +p Nil{}:
151      {==}
152    case 1n+ +p Con{+x, t}:
153      %Equal.sym(Maybe<&2, Nat>, SF.from_le(p, t), None{}, fl_len(p, t, h)) : {SF.digit_on(_, C.fits(8n, x), x) == None{} : Maybe<&2, Nat>}
154      {==}