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
|
Require Import Int63.
Set Implicit Arguments.
Open Scope int63_scope.
Check (eq_refl : diveucl_21 1 1 2 = (4611686018427387904,1)).
Check (eq_refl (4611686018427387904,1) <: diveucl_21 1 1 2 = (4611686018427387904,1)).
Check (eq_refl (4611686018427387904,1) <<: diveucl_21 1 1 2 = (4611686018427387904,1)).
Definition compute1 := Eval compute in diveucl_21 1 1 2.
Check (eq_refl compute1 : (4611686018427387904,1) = (4611686018427387904,1)).
Check (eq_refl : diveucl_21 3 1 2 = (0, 0)).
Check (eq_refl (0, 0) <: diveucl_21 3 1 2 = (0, 0)).
Check (eq_refl (0, 0) <<: diveucl_21 3 1 2 = (0, 0)).
Definition compute2 := Eval compute in diveucl_21 3 1 2.
Check (eq_refl compute2 : (0, 0) = (0, 0)).
Check (eq_refl : diveucl_21 1 1 0 = (0,0)).
Check (eq_refl (0,0) <: diveucl_21 1 1 0 = (0,0)).
Check (eq_refl (0,0) <<: diveucl_21 1 1 0 = (0,0)).
Check (eq_refl : diveucl_21 9223372036854775807 0 1 = (0,0)).
Check (eq_refl (0,0) <: diveucl_21 9223372036854775807 0 1 = (0,0)).
Check (eq_refl (0,0) <<: diveucl_21 9223372036854775807 0 1 = (0,0)).
Check (eq_refl : diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
Check (eq_refl (17407905077428, 3068214991893055266) <: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
Check (eq_refl (17407905077428, 3068214991893055266) <<: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
|
