def all_hold

stelliferous@0.0.2.0 · proofs/boolean_logic.bend:43

import Base
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape

43def all_hold(+conditions: List<&2,Bool>,+holds: Holds(conditions)) -> {all(conditions) == True{} : Bool}:
44  match conditions:
45    case Nil{}: {==}
46    case +last <> +prefix:
47      Shape.Both{+here,+rest} = holds
48      %Equal.sym(Bool,all(prefix),True{},all_hold(prefix,rest)) : {Bool.and(_,last) == True{} : Bool}
49      here