Tensor.Bool.check: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/tensor.bend as Tensor
Lines 94-100 of bendtorch@1.3.0.0/tensor.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/tensor.bend&start_line=94&end_line=100

import Base

# a proof that b is True, when it is: where shapes read at run time enter, a program checks a condition once
def Bool.check(b: Bool) -> Maybe<&1, {True{} == b : Bool}>:
  match b:
    case True{}:
      Some{{==}}
    case False{}:
      None{}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe