~/jendhub

def internal_range_go_append

bend-mathlib@0.8.1.0 · list.bend:1980

import bend-mathlib@0.8.1.0/list.bend as List
import Base

1980def internal_range_go_append(+n: Nat, -ys: List<&2, Nat>, -acc: List<&2, Nat>) -> {List.range.go(n, List.append(&2, Nat, ys, acc)) == List.append(&2, Nat, List.range.go(n, ys), acc) : List<&2, Nat>}:
1981  match n:
1982    case 0n:
1983      {==}
1984    case 1n+p:
1985      internal_range_go_append(p, p <> ys, acc)

Uses (4)

Used by (1)