Commit 273e31f5 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Remove dk_binary_nat.length: This was nonsense since 0 = S0 0 have no finite length

parent 398522c6
...@@ -98,11 +98,6 @@ def div2 : BNat -> BNat. ...@@ -98,11 +98,6 @@ def div2 : BNat -> BNat.
[n] div2 (S0 n) --> n [n] div2 (S0 n) --> n
[n] div2 (S1 n) --> n. [n] div2 (S1 n) --> n.
def length : BNat -> UNat.
[] length O --> dk_nat.O
[n] length (S0 n) --> dk_nat.S (length n)
[n] length (S1 n) --> dk_nat.S (length n).
(; quo2 n k = n / 2^k ;) (; quo2 n k = n / 2^k ;)
def quo2 : BNat -> UNat -> BNat. def quo2 : BNat -> UNat -> BNat.
[n] quo2 n dk_nat.O --> n [n] quo2 n dk_nat.O --> n
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment