def bool.and2

bend-osdev-caps@0.1.0.0 · PROOF.bend:101

import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
import Base

101def bool.and2(+x: Bool, +y: Bool) -> {x == True{} : Bool} -> {y == True{} : Bool} -> {Bool.and(x, y) == True{} : Bool}:
102  match x:
103    case True{}:
104      hx => hy => hy
105    case False{}:
106      hx => hy => bits.absurd(Bool.and(False{}, y), hx)

Uses (3)

Used by (1)