def and_left

bendtorch-core@0.1.0.0 · src/storage/arith.bend:468

import Base

468def and_left(+a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
469  match a:
470    case False{}:
471      Empty.absurd({False{} == True{} : Bool}, clash(h))
472    case True{}:
473      {==}