Home
About Coq
Get Coq
Documentation
Community
The Coq Proof Assistant
Library Ltac2.Uint63
Require
Import
Ltac2.Init
.
Ltac
2
Type
t
:=
uint63
.
Ltac
2 @
external
equal
:
t
->
t
->
bool
:= "coq-core.plugins.ltac2" "uint63_equal".
Navigation
Standard Library
Table of contents
Index