Commit b84fcb1e authored by Jan's avatar Jan
Browse files

renamed list because l and 1 were indistinguishable

parent fecd9cf4
Pipeline #48277 passed with stage
in 4 minutes and 57 seconds
......@@ -200,7 +200,7 @@ Section sum_list.
Proof.
induction l; simpl; rewrite ?reverse_cons, ?sum_list_with_app; simpl; lia.
Qed.
Lemma sum_list_with_in x (f : A nat) l : x l f x sum_list_with f l.
Lemma sum_list_with_in x (f : A nat) ls : x ls f x sum_list_with f ls.
Proof. induction 1; simpl; lia. Qed.
Lemma join_reshape szs l :
sum_list szs = length l mjoin (reshape szs l) = l.
......
Supports Markdown
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