def map_when
stelliferous@0.0.2.0 · proofs/traversal_lanes_certificate.bend:18
import stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend as TraversalLanesCertificate
import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as LanesWitness
18def map_when(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,-values: Array<F32>,
19 certificate: Certificate.Certificate<F32,values>) -> Certificate.Certificate<F32,Lanes.map_when(~Context,~operation,covered,count,position,context,values)>:
20 Certificate.Certificate{+depth,equation} = certificate
21 Certificate.Certificate{depth,
22 %Certificate.restored(F32,depth,Lanes.map_when(~Context,~operation,covered,count,position,context,values),
23 LanesWitness.map_when(~Context,~operation,covered,depth,count,position,context,values,Certificate.witness_at(F32,depth,values,equation))) :
24 {_ == Tree.pack(F32,Certificate.normalized(F32,depth,Tree.reflect(F32,Lanes.map_when(~Context,~operation,covered,count,position,context,values)))) : Array<F32>}
25 {==}}