diff options
| author | Reynald Affeldt | 2019-10-25 01:01:10 +0900 |
|---|---|---|
| committer | Cyril Cohen | 2019-12-11 14:26:52 +0100 |
| commit | 81a3634d0b72262fd8e6299bc94d9a7ab31ce3c0 (patch) | |
| tree | 24edc74bc44f939834614512dd0a963f06363b2d /mathcomp/algebra | |
| parent | 843e345d5d8217a02de9e7fe20406b83074e807d (diff) | |
editing documentation in order.v and ssrnum.v
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 5737a2d..6bbf24a 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -6,7 +6,10 @@ From mathcomp Require Import ssralg poly. (******************************************************************************) (* This file defines some classes to manipulate number structures, i.e *) -(* structures with an order and a norm. *) +(* structures with an order and a norm. To use this file, insert *) +(* "Import Num.Theory." before your scripts. You can also "Import Num.Def." *) +(* to enjoy shorter notations (e.g., minr instead of Num.min, lerif instead *) +(* of Num.leif, etc.). *) (* *) (* * NumDomain (Integral domain with an order and a norm) *) (* numDomainType == interface for a num integral domain. *) |