def finish

stelliferous@0.0.2.0 · proofs/kernel_tile_witness.bend:21

import Base
import stelliferous@0.0.2.0/kernel_block.bend as Block
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

21def finish(~State: Type,-state: State,-result: State & Block.Twin<Block.Twin<Block.Twin<F32>>>,
22  evidence: TraversalWitness.Sample<State,Block.Twin<Block.Twin<Block.Twin<F32>>>,state,result>) ->
23  TraversalWitness.Sample<State,Tile.Tile8,state,Tile.finish_pairs(~State,result)>:
24  TraversalWitness.Sample{value,equation} = evidence
25  %Equal.sym(State & Block.Twin<Block.Twin<Block.Twin<F32>>>,result,(state,value),equation) :
26    TraversalWitness.Sample<State,Tile.Tile8,state,Tile.finish_pairs(~State,_)>
27  TraversalWitness.Sample{Tile.pairs_value(value),{==}}