def leaf_facts

bendtorch-core@0.1.0.0 · src/tensor/parallel_proofs.bend:59

import Base
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Build

59def leaf_facts(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
60  +p: P, -start: (A & B), +count: Nat, +base: Nat, pair: F32 & (A & B),
61  -exact: {pair == cell(p, base, start, Nat.is_lt(base, count)) : F32 & (A & B)},
62  -keeps: Keeps(~P, ~A, ~B, ~cell, p, start)) ->
63  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 0n, count, base, Build.leaf(~(A & B), pair))>:
64  (value, rest) = pair
65  Fact{(Equal.trans((A & B), rest, Pair.snd(F32, (A & B), cell(p, base, start, Nat.is_lt(base, count))), start,
66      Equal.cong(F32 & (A & B), (A & B), q => Pair.snd(F32, (A & B), q), (value, rest), cell(p, base, start, Nat.is_lt(base, count)), exact),
67      keeps(base)(Nat.is_lt(base, count))),
68    path => Equal.cong(F32 & (A & B), Maybe<&2, F32>, q => Some{Pair.fst(F32, (A & B), q)}, (value, rest),
69      cell(p, base, start, Nat.is_lt(base, count)), exact))}