diff options
| author | Pierre Boutillier | 2014-09-08 17:35:50 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-10-01 23:24:36 +0200 |
| commit | b9cbf680f13927340720d1d0f4938dcc6cd65d1f (patch) | |
| tree | 7cc258ea9458122d4e333f6cfa7af8a792242824 /theories/Init | |
| parent | f640bcbe834cef3559118a093f1a905cacdccc2f (diff) | |
eta contractions
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Nat.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index 5764b349b6..dddc0fc336 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -280,8 +280,8 @@ Fixpoint testbit a n : bool := | S n => testbit (div2 a) n end. -Definition shiftl a n := iter n double a. -Definition shiftr a n := iter n div2 a. +Definition shiftl a := nat_rect _ a (fun _ => double). +Definition shiftr a := nat_rect _ a (fun _ => div2). Fixpoint bitwise (op:bool->bool->bool) n a b := match n with |