Require Import Ltac2.Init.
Ltac2
Type exn ::= [
Division_by_zero ].
Ltac2 @
external equal :
int ->
int ->
bool := "ltac2" "int_equal".
Ltac2 @
external compare :
int ->
int ->
int := "ltac2" "int_compare".
Ltac2 @
external add :
int ->
int ->
int := "ltac2" "int_add".
Ltac2 @
external sub :
int ->
int ->
int := "ltac2" "int_sub".
Ltac2 @
external mul :
int ->
int ->
int := "ltac2" "int_mul".
Ltac2 @
external neg :
int ->
int := "ltac2" "int_neg".
Ltac2
lt (
x :
int) (
y :
int) :=
equal (
compare x y) -1.
Ltac2
gt (
x :
int) (
y :
int) :=
equal (
compare x y) 1.
Ltac2
le (
x :
int) (
y :
int) :=
match equal x y with
|
true =>
true
|
false =>
lt x y
end.
Ltac2
ge (
x :
int) (
y :
int) :=
match equal x y with
|
true =>
true
|
false =>
gt x y
end.