KernelTileWitness.finish: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend as KernelTileWitness
Lines 21-27 of stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend&start_line=21&end_line=27

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

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

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_block.bend&name=Twin
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=Tile8
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=finish_pairs
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_tile.bend&name=pairs_value
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=Sample