type b_L1RF

bendtorch@1.3.0.0 · PROOF.bend:721

import Base
import bendtorch@1.3.0.0/main.bend as T

721type b_L1RF<-h: Nat, -dm: T.Dm, -xs: List<&1, T.BG>, -acc: List<&1, T.DB>> is Type:
722  b_L1RF{ys: List<&1, T.BG>, same: {ys == xs : List<&1, T.BG>}, fact: {T.bleaf_full(xs, h, dm, acc) == List.reverse.go(&1, T.DB, acc, b_ffmap(h, dm, xs)) : List<&1, T.DB>}}