~/bend-docscommunity

proofs/word_width.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/word_width.bend as Word_width

Width transport changes the type index, never the stored bits.

1 import
import Base

Laws

law transport_cons provedsource · line 8 · raw

@+source:Nat -> @+target:Nat -> @+bit:Bool -> @+tail:Word(source) -> @width:{source == target : Nat} -> {transport(1n+source, 1n+target, WCon{bit, tail}, Equal.cong(Nat, Nat, n => 1n+n, source, target, width)) == WCon{bit, transport(source, target, tail, width)} : Word(1n+target)}

Definitions

def transport source · line 4 · raw

@-source:Nat -> @-target:Nat -> @value:Word(source) -> @width:{source == target : Nat} -> Word(target)