baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2022-12-10 14:56:42 +01:00
parent 2489ad0497
commit dc91289017
1 changed files with 0 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
thue-morse.v
View File

@ -1416,30 +1416,6 @@ Require Import BinPos.
(*
PeanoNat.Nat.log2_spec_alt:
forall a : nat,
0 < a ->
exists r : nat,
a = 2 ^ PeanoNat.Nat.log2 a + r /\ 0 <= r < 2 ^ PeanoNat.Nat.log2 a
N.log2_spec_alt:
forall a : N,
(0 < a)%N ->
exists r : N, a = (2 ^ N.log2 a + r)%N /\ (0 <= r < 2 ^ N.log2 a)%N
PeanoNat.Nat.log2_shiftl:
forall a n : nat,
a <> 0 ->
PeanoNat.Nat.log2 (PeanoNat.Nat.shiftl a n) = PeanoNat.Nat.log2 a + n
*)
(* Hamming weight of a positive; argument can not be 0! *) (* Hamming weight of a positive; argument can not be 0! *)
Fixpoint hamming_weight_positive (x: positive) := Fixpoint hamming_weight_positive (x: positive) :=
match x with match x with