AlphaGitHub
Source/Packages

Runtime.ArenaCertificate

packages/execution/src/Runtime/ArenaCertificate.alpha

331 lines63 declarations18.7 KiBSHA-256 3018604760e2
Download exact fileView at revision426597bda5753d86c4

def · lines 141–148

arenaRangesMeet

Full file
1 when [start, stop) meets a range of the list
141def arenaRangesMeet =
142  (lambda unrestricted start : Nat .
143    (lambda unrestricted stop : Nat .
144      (lambda unrestricted ranges : (family ArenaRanges) .
145        (eliminate ArenaRanges (lambda unrestricted current : (family ArenaRanges) . Nat) ranges
146          (branch ArenaRangesNone . 0)
147          (branch ArenaRangesNext otherStart otherStop tail induction .
148            (naturalOr (naturalAnd (naturalLess start otherStop) (naturalLess otherStart stop)) induction))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.