List.internal_all_reverse_go: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/list.bend as List
Lines 1534-1546 of bend-mathlib@0.8.1.0/list.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/list.bend&start_line=1534&end_line=1546

import Base
import bend-mathlib@0.8.1.0/bool.bend as MBool

def internal_all_reverse_go(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>, -acc: List<a, A>, c: Bool, e: {List.all(~a, ~A, ~f, acc) == c : Bool}) -> {List.all(~a, ~A, ~f, List.reverse.go(a, A, xs, acc)) == Bool.and(c, List.all(~a, ~A, ~f, xs)) : Bool}:
  match xs c:
    case Nil{} True{}:
      e
    case Nil{} False{}:
      e
    case h <> t True{}:
      +v = f(h)
      %internal_all_cons_test(~a, ~A, ~f, h, t, v, {==}) : {List.all(~a, ~A, ~f, List.reverse.go(a, A, t, h <> acc)) == _ : Bool}
      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, List.all(~a, ~A, ~f, h <> acc), Bool.and(v, List.all(~a, ~A, ~f, acc)), v, Equal.sym(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), List.all(~a, ~A, ~f, h <> acc), internal_all_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, True{}), v, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), True{}, e), MBool.and_true(v))))
    case h <> t False{}:
      +v = f(h)
      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, False{}, Equal.trans(Bool, List.all(~a, ~A, ~f, h <> acc), Bool.and(v, List.all(~a, ~A, ~f, acc)), False{}, Equal.sym(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), List.all(~a, ~A, ~f, h <> acc), internal_all_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, False{}), False{}, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), False{}, e), MBool.and_false(v))))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.all
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse.go
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_false
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/bool.bend&name=and_true
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=internal_all_cons_test