Istari

Symbol

The symbol type:

symbol : U 0

Symbol literals are written using a sym` parsing directive and a string lexeme. For example, sym`"foo".

The only operation on symbols is equality:

symbol_eqb : symbol -> symbol -> bool

istrue_symbol_eqb : forall (s t : symbol) . Bool.istrue (symbol_eqb s t) <-> s = t : symbol