diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-10-25 17:43:00 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-10-25 17:43:00 +0100 |
| commit | f2d2bbd4a759024b716cc7f802427fdb78edfb9d (patch) | |
| tree | 85ac91ec5631bb36bbdb16f8676183a771273c7f /src/common | |
| parent | 20749ef047b5a7189f6f52227e8d4f98c0c6370e (diff) | |
| download | vericert-f2d2bbd4a759024b716cc7f802427fdb78edfb9d.tar.gz vericert-f2d2bbd4a759024b716cc7f802427fdb78edfb9d.zip | |
Add proofs for sem_pexpr and app_predicated
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/NonEmpty.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 923a637..31adbda 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -62,6 +62,7 @@ Fixpoint non_empty_prod {A B} (l: non_empty A) (l': non_empty B) := Fixpoint of_list {A} (l: list A): option (non_empty A) := match l with + | a::nil => Some (singleton a) | a::b => match of_list b with | Some b' => Some (a ::| b') |