package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Extend.MakeSource

Parameters

module D : Sig.Minimal

Signature

Sourceval imperative_assume : D.Context.t -> D.boolean -> unit

Because the transfer functions imperatively change the context, they cannot use assume, that returns a new context. Temporarily, we provide this instead (it should be applied only to fresh symbolic variables and not modify the set of valuations of the other symbolic variables. In particular, the condition must never make the context bottom).

The good long-term solution would be to make every transfer function return a new Context.t option, viewing the context as some state monad.