mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-26 16:20:40 +03:00
Remove dead code
This commit is contained in:
parent
a3de14763b
commit
52c6cb4f01
@ -1,2 +1,2 @@
|
||||
Word.leading_ones<size: Nat>(word: Word(size)): Nat
|
||||
Word.leading_ones.go<size>(word, 0, 0)
|
||||
Word.leading_ones.go<size>(word, 0)
|
||||
|
@ -1,6 +1,6 @@
|
||||
Word.leading_ones.go<size: Nat>(word: Word(size), c: Nat, n: Nat): Nat
|
||||
Word.leading_ones.go<size: Nat>(word: Word(size), n: Nat): Nat
|
||||
case word {
|
||||
e: n,
|
||||
o: Word.leading_ones.go<word.size>(word.pred, Nat.succ(c), 0),
|
||||
i: Word.leading_ones.go<word.size>(word.pred, Nat.succ(c), Nat.succ(n))
|
||||
o: Word.leading_ones.go<word.size>(word.pred, 0),
|
||||
i: Word.leading_ones.go<word.size>(word.pred, Nat.succ(n))
|
||||
}: Nat
|
||||
|
@ -1,2 +1,2 @@
|
||||
Word.leading_zeros<size: Nat>(word: Word(size)): Nat
|
||||
Word.leading_zeros.go<size>(word, 0, 0)
|
||||
Word.leading_zeros.go<size>(word, 0)
|
||||
|
@ -1,6 +1,6 @@
|
||||
Word.leading_zeros.go<size: Nat>(word: Word(size), c: Nat, n: Nat): Nat
|
||||
Word.leading_zeros.go<size: Nat>(word: Word(size), n: Nat): Nat
|
||||
case word {
|
||||
e: n,
|
||||
o: Word.leading_zeros.go<word.size>(word.pred, Nat.succ(c), Nat.succ(n)),
|
||||
i: Word.leading_zeros.go<word.size>(word.pred, Nat.succ(c), 0)
|
||||
o: Word.leading_zeros.go<word.size>(word.pred, Nat.succ(n)),
|
||||
i: Word.leading_zeros.go<word.size>(word.pred, 0)
|
||||
}: Nat
|
||||
|
@ -1,2 +1,2 @@
|
||||
Word.trailing_ones<size: Nat>(word: Word(size)): Nat
|
||||
Word.trailing_ones.go<size>(word, 0, 0)
|
||||
Word.trailing_ones.go<size>(word, 0)
|
||||
|
@ -1,6 +1,6 @@
|
||||
Word.trailing_ones.go<size: Nat>(word: Word(size), c: Nat, n: Nat): Nat
|
||||
Word.trailing_ones.go<size: Nat>(word: Word(size), n: Nat): Nat
|
||||
case word {
|
||||
e: n
|
||||
o: n,
|
||||
i: Word.trailing_ones.go<word.size>(word.pred, Nat.succ(c), Nat.succ(n))
|
||||
i: Word.trailing_ones.go<word.size>(word.pred, Nat.succ(n))
|
||||
}: Nat
|
||||
|
@ -1,2 +1,2 @@
|
||||
Word.trailing_zeros<size: Nat>(word: Word(size)): Nat
|
||||
Word.trailing_zeros.go<size>(word, 0, 0)
|
||||
Word.trailing_zeros.go<size>(word, 0)
|
||||
|
@ -1,6 +1,6 @@
|
||||
Word.trailing_zeros.go<size: Nat>(word: Word(size), c: Nat, n: Nat): Nat
|
||||
Word.trailing_zeros.go<size: Nat>(word: Word(size), n: Nat): Nat
|
||||
case word {
|
||||
e: n
|
||||
o: Word.trailing_zeros.go<word.size>(word.pred, Nat.succ(c), Nat.succ(n)),
|
||||
o: Word.trailing_zeros.go<word.size>(word.pred, Nat.succ(n)),
|
||||
i: n
|
||||
}: Nat
|
||||
|
Loading…
Reference in New Issue
Block a user