LAWS.latest: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as LAWS
Lines 142-153 of bendtorch-core@0.1.0.0/src/storage/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&start_line=142&end_line=153

import Base

def latest(+n: Nat, op: Op, +j: U32, value: F32) -> F32:
  match op:
    case Write{+i, new}:
      Bool.pick(F32, Bool.and(Nat.is_lt(U32.to_nat(i), n), Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), new, value)
    case Read{i}:
      value
    case First{}:
      value
    case Second{}:
      value
    case Length{}:
      value

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op