def append_nil

bendtorch-core@0.1.0.0 · src/tensor/contracts/pointwise_proof.bend:15

import Base
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws

15def append_nil(+ops: List<&2, StorageLaws.Op>) -> {List.append(&2, StorageLaws.Op, ops, Nil{}) == ops : List<&2, StorageLaws.Op>}:
16  match ops:
17    case Nil{}:
18      {==}
19    case +op <> +rest:
20      Equal.cong(List<&2, StorageLaws.Op>, List<&2, StorageLaws.Op>, tail => op <> tail,
21        List.append(&2, StorageLaws.Op, rest, Nil{}), rest, append_nil(rest))