def none_some

bend-collections-laws-math@1.0.0.0 · proofs/lib/logic.bend:80

import Base

80# Maybe discrimination.
81def none_some(-A: Data, x: A, e: {None{} == Some{x} : Maybe<&2, A>}) -> Empty:
82  %Equal.sym(Maybe<&2, A>, None{}, Some{x}, e) : truth(Maybe.is_some(&2, A, _))
83  Unit{}