PROOF.b_MRF: type of bendtorch@1.3.0.0 Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF Lines 755-756 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=755&end_line=756 import Base import bendtorch@1.3.0.0/main.bend as T type b_MRF<-d: Nat, -gs: T.Halves, -n: Nat, -h: Nat, -dm: T.Dm> is Type: b_MRF{ys: List<&1, T.BG>, same: {ys == T.hcat(T.BG, gs) : List<&1, T.BG>}, fact: {T.bpar_full(d, gs, n, h, dm) == b_ffmap(h, dm, T.hcat(T.BG, gs)) : List<&1, T.DB>}} Uses (9): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_ffmap https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=BG https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=DB https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Dm https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Halves https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=bpar_full https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=hcat