Function creusot_contracts::util::such_that

source · 
pub fn such_that<T>(p: Mapping<T, bool>) -> T
Expand description

Creates a logical value satisfying the property given by p.

This is also called the “epsilon operator”: its goal is not extract from ∃x. P(x) a x satisfying P.

logic ⚠

requires 

exists<x: T> p[x]

ensures 

p[result]