def some_none

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:31

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

31def some_none(-A: Data, -x: A, equal: {Some{x} == None{} : Maybe<&2, A>}) -> Empty:
32  Shape.clash(Equal.cong(Maybe<&2, A>, Bool, found => Maybe.is_some(&2, A, found), Some{x}, None{}, equal))