Compiler.Lexer

69def classifyByte =
70  (lambda unrestricted byte : Byte .
71    (nat-eliminate
72      (lambda unrestricted matchedOpen : Nat . (family ByteClass))
73      (nat-eliminate
74        (lambda unrestricted matchedClose : Nat . (family ByteClass))
75        (nat-eliminate
76          (lambda unrestricted matchedWhitespace : Nat . (family ByteClass))
77          (nat-eliminate
78            (lambda unrestricted matchedDigit : Nat . (family ByteClass))
79            (constructor ByteClass IdentifierByte)
80            (lambda unrestricted predecessor : Nat .
81              (lambda unrestricted induction : (family ByteClass) .
82                (constructor ByteClass DecimalDigit)))
83            (isDecimalDigit byte))
84          (lambda unrestricted predecessor : Nat .
85            (lambda unrestricted induction : (family ByteClass) .
86              (constructor ByteClass Whitespace)))
87          (isWhitespace byte))
88        (lambda unrestricted predecessor : Nat .
89          (lambda unrestricted induction : (family ByteClass) .
90            (constructor ByteClass CloseDelimiter)))
91        (byte-equal byte (byte 41)))
92      (lambda unrestricted predecessor : Nat .
93        (lambda unrestricted induction : (family ByteClass) . (constructor ByteClass OpenDelimiter)))
94      (byte-equal byte (byte 40))))