def and_l

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2004

import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF

import Base

2004def and_l(+a: Bool, +b: Bool, +e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
2005  match a:
2006    case True{}:
2007      {==}
2008    case False{}:
2009      Empty.absurd({False{} == True{} : Bool}, ft_absurd(e))

Uses (4)

Used by (6)