law show_fin

lawful-fields@0.1.1.0 · proof_digits.bend:262

import Base
import lawful-fields@0.1.1.0/defs.bend as F

262law show_fin:
263  for +g: Nat
264  for +q: Nat
265  for +d: U32
266  for +sacc: String
267  {F.codes(Nat.show.fin(g, sacc, (Chr{d}, q))) == lgo(g, q, d, F.codes(sacc)) : List<&2, U32>}