law tab_exp_rs

bend-osdev-gf@0.1.1.0 · LAWS.bend:173

import bend-osdev-gf@0.1.1.0/LAWS.bend as LAWS
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-osdev-gf@0.1.1.0/tables.bend as T

173law tab_exp_rs:
174  for +i: U32
175  for +hi: {Nat.is_lt(U32.to_nat(i), 510n) == True{} : Bool}
176  {T.Gf8Tab.exp(T.Gf8Tab.new(G.Gf8.rs()), i) == (T.Gf8Tab.new(G.Gf8.rs()), G.Gf8.exp(G.Gf8.rs(), U32.to_nat(i))) : T.Gf8Tab & U32}

Uses (14)

Used by (0)

No other definition uses this definition.