BooleanLogic.all_hold: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/boolean_logic.bend as BooleanLogic
Lines 43-49 of stelliferous@0.0.2.0/proofs/boolean_logic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&start_line=43&end_line=49

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

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

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/boolean_logic.bend&name=all
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Both