AlphaGitHub
Source/Packages

Data.UTF8

packages/foundation/standard/src/Data/UTF8.alpha

1,298 lines193 declarations53.6 KiBSHA-256 4bef3dfd330d
Download exact fileView at revisionf5034773ad4bb52133

def · lines 703–721

utf8CodepointsReverse

Full file
Reverse a codepoint list in O(length). `fuel` need only be an upper bound on the list length (the caller passes the input byte count, always >= the codepoint count); once the list is exhausted the state stops changing.
703def utf8CodepointsReverse =
704  (lambda unrestricted fuel : Nat .
705    (lambda unrestricted list : (family UTF8Codepoints) .
706      (eliminate
707        UTF8CodepointsReverseState
708        (lambda unrestricted current : (family UTF8CodepointsReverseState) .
709          (family UTF8Codepoints))
710        (nat-eliminate
711          (lambda unrestricted step : Nat . (family UTF8CodepointsReverseState))
712          (constructor
713            UTF8CodepointsReverseState
714            UTF8CodepointsReverseStateValue
715            list
716            (constructor UTF8Codepoints UTF8CodepointsEnd))
717          (lambda unrestricted predecessor : Nat .
718            (lambda unrestricted induction : (family UTF8CodepointsReverseState) .
719              (utf8CodepointsReverseStep induction)))
720          fuel)
721        (branch UTF8CodepointsReverseStateValue remaining accumulated . accumulated))))

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.