def lift

stelliferous@0.0.2.0 · proofs/storage_buffer_model.bend:149

import Base
import stelliferous@0.0.2.0/storage_buffer.bend as Storage

149def lift(~Element: Data,~Context: Data,~Proposition: Context -> @-buffer: Storage.Buffer<Element> -> Type,+context: Context,-buffer: Storage.Buffer<Element>,
150  observation: Observation<Element,buffer>,canonical: @+model: Model<Element> -> Proposition(context,pack(~Element,model))) -> Proposition(context,buffer):
151  Observation{model,equation} = observation
152  %equation : Proposition(context,_)
153  canonical(model)