def WN

lawful-fields@0.1.1.0 · proof_cut.bend:329

import lawful-fields@0.1.1.0/proof_cut.bend as ProofCut

import Base

329def WN(ns: List<&2, Nat>, +from: Nat, +to: Nat) -> Bool:
330  match ns:
331    case Nil{}:
332      True{}
333    case Con{+e, t}:
334      (Nat.is_le(from, e) && Nat.is_le(e, to)) && WN(t, from, to)

Uses (5)

Used by (6)