lean4-htt/doc/char.md
John Tristan f237fb67eb
doc: documenting Char and upstreaming extensionality from batteries (#4438)
* Basic documentation for characters
* Upstreamed two extensionality theorems from batteries

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
2024-06-16 00:43:34 +00:00

496 B

Characters

A value of type Char, also known as a character, is a Unicode scalar value. It is represented using an unsigned 32-bit integer and is statically guaranteed to be a valid Unicode scalar value.

Syntactically, character literals are enclosed in single quotes.

#eval 'a' -- 'a'
#eval '∀' -- '∀'

Characters are ordered and can be decidably compared using the relational operators =, <, , >, .