Skip to content
Snippets Groups Projects
Commit c9edf9a0 authored by Michael Sammler's avatar Michael Sammler
Browse files

fix implicit types

parent cf70f15e
No related branches found
No related tags found
1 merge request!254Add little endian encoding of Z
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/list_numbers.v
+ 2
− 2
View file @ c9edf9a0
...@@ -218,8 +218,8 @@ End sum_list. ...@@ -218,8 +218,8 @@ End sum_list.
(** ** Properties of the [Z_to_little_endian] and [Z_of_little_endian] functions *) (** ** Properties of the [Z_to_little_endian] and [Z_of_little_endian] functions *)
Section Z_little_endian. Section Z_little_endian.
Local Open Scope Z_scope. Local Open Scope Z_scope.
Implicit Types n m : nat. Implicit Types m : nat.
Implicit Types z : Z. Implicit Types n z : Z.
Lemma Z_to_of_little_endian m n bs: Lemma Z_to_of_little_endian m n bs:
m = length bs → 0 ≤ n → m = length bs → 0 ≤ n →
......
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