Home
About Coq
Get Coq
Documentation
Community
The Coq Proof Assistant
Library Ltac2.Char
Require
Import
Ltac2.Init
.
Ltac
2 @
external
of_int
:
int
->
char
:= "ltac2" "char_of_int".
Ltac
2 @
external
to_int
:
char
->
int
:= "ltac2" "char_to_int".
Navigation
Standard Library
Table of contents
Index