~/jendhub

def gc.elt0

bend-osdev-gf@0.1.1.0 · proof_tab_cases.bend:2093

import bend-osdev-gf@0.1.1.0/proof_tab_cases.bend as ProofTabCases
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

2093def gc.elt0(+a: U32, h: {U32.is_eq(G.Gf8.elt(a), 0) == True{} : Bool}) -> {G.Gf8.elt(a) == 0 : U32}:
2094  match a:
2095    case U32{WCon{+b0, WCon{+b1, WCon{+b2, WCon{+b3, WCon{+b4, WCon{+b5, WCon{+b6, WCon{+b7, +r}}}}}}}}}:
2096      gc.elt0.bits(b0, b1, b2, b3, b4, b5, b6, b7, h)

Uses (6)

Used by (1)