diff options
Diffstat (limited to 'theories/NArith/BinNatDef.v')
| -rw-r--r-- | theories/NArith/BinNatDef.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index d459f8509..d7660422a 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -181,6 +181,14 @@ Definition pow n p := Infix "^" := pow : N_scope. +(** Square *) + +Definition square n := + match n with + | 0 => 0 + | Npos p => Npos (Pos.square p) + end. + (** Base-2 logarithm *) Definition log2 n := |