Export.v 1.05 KB
Newer Older
1
2
3
4
From Tweetnacl Require Export Libs.LibTactics_SF.
From Tweetnacl Require Export Libs.LibTactics_Rennes.
From Tweetnacl Require Export Libs.LibTactics.
From Tweetnacl Require Export Libs.Lists_extended.
5
From Tweetnacl Require Export Libs.Logic_extended.
6
7
8
9
10
From Tweetnacl Require Export Libs.Decidable.
From Tweetnacl Require Export Libs.Term_Decidable.
From Tweetnacl Require Export Libs.Expr_Decidable.
From Tweetnacl Require Export Libs.List_Decidable.
From Tweetnacl Require Export Libs.List_ext_Decidable.
11
12
13
14
From Tweetnacl Require Export Libs.List_Ltac.
From Tweetnacl Require Export Libs.Forall_extended.
From Tweetnacl Require Export Libs.ZArith_extended.
From Tweetnacl Require Export Libs.Relations.
15
(* Require Export mathcomp.ssreflect.ssreflect. *)
16
17
18
19
20
21
Require Export Coq.ZArith.BinInt.
Require Export Coq.ZArith.Zdiv.

Open Scope Z.

Notation "ℤ.ℕ A" := (Z.of_nat A) (at level 60, right associativity).
22
23
24
25
Notation "A :𝓖𝓕" := (A mod (2^255 - 19)) (at level 40, left associativity).
(*Print Grammar pattern.*)
Notation  := nat.
Notation  := Z.
26
27

Close Scope Z.