def and_right

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

import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

import Base

475def and_right(+a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
476  match a:
477    case False{}:
478      Empty.absurd({b == True{} : Bool}, clash(h))
479    case True{}:
480      h

Uses (4)

Used by (30)