Skip to content
Snippets Groups Projects
Commit 773f2fc5 authored by Alban Gruin's avatar Alban Gruin
Browse files

utils: cleanup


Signed-off-by: default avatarAlban Gruin <alban.gruin@irit.fr>
parent b8bd03d3
No related branches found
No related tags found
No related merge requests found
Require Import Lia List Nat.
Import ListNotations.
Scheme Equality for list.
Lemma list_elt_exists :
forall (A : Type) (l : list A) (d : A) i,
i < List.length l -> (exists a, List.nth_error l i = Some a).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment