1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Ltac2.Init.
Ltac2 Type t := int.
Ltac2 @ external equal : int -> int -> bool := "coq-core.plugins.ltac2" "int_equal".
Ltac2 @ external compare : int -> int -> int := "coq-core.plugins.ltac2" "int_compare".
Ltac2 @ external add : int -> int -> int := "coq-core.plugins.ltac2" "int_add".
Ltac2 @ external sub : int -> int -> int := "coq-core.plugins.ltac2" "int_sub".
Ltac2 @ external mul : int -> int -> int := "coq-core.plugins.ltac2" "int_mul".
(* Note: unlike Coq Z division, Ltac2 matches OCaml division and rounds towards 0, so 1/-2 = 0 *)
Ltac2 @ external div : int -> int -> int := "coq-core.plugins.ltac2" "int_div".
Ltac2 @ external mod : int -> int -> int := "coq-core.plugins.ltac2" "int_mod".
Ltac2 @ external neg : int -> int := "coq-core.plugins.ltac2" "int_neg".
Ltac2 @ external abs : int -> int := "coq-core.plugins.ltac2" "int_abs".
Ltac2 @ external asr : int -> int -> int := "coq-core.plugins.ltac2" "int_asr".
Ltac2 @ external lsl : int -> int -> int := "coq-core.plugins.ltac2" "int_lsl".
Ltac2 @ external lsr : int -> int -> int := "coq-core.plugins.ltac2" "int_lsr".
Ltac2 @ external land : int -> int -> int := "coq-core.plugins.ltac2" "int_land".
Ltac2 @ external lor : int -> int -> int := "coq-core.plugins.ltac2" "int_lor".
Ltac2 @ external lxor : int -> int -> int := "coq-core.plugins.ltac2" "int_lxor".
Ltac2 @ external lnot : int -> int := "coq-core.plugins.ltac2" "int_lnot".
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) :=
(* we might use [lt x (add y 1)], but that has the wrong behavior on MAX_INT *)
match equal x y with
| true => true
| false => lt x y
end.
Ltac2 ge (x : int) (y : int) :=
(* we might use [lt (add x 1) y], but that has the wrong behavior on MAX_INT *)
match equal x y with
| true => true
| false => gt x y
end.
|
