def pk_t

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:35

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF

35# SF.pick on a known Bool, as lemmas: rewriting with these keeps a conversion
36# syntactic instead of unfolding (and normalizing) both branches
37def pk_t(-T: Data, +a: T, +b: T) -> {SF.pick(T, True{}, a, b) == a : T}:
38  {==}