def and_r

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

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

import Base

2011def and_r(+a: Bool, +b: Bool, +e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
2012  match a:
2013    case True{}:
2014      e
2015    case False{}:
2016      Empty.absurd({b == True{} : Bool}, ft_absurd(e))

Uses (4)

Used by (2)