Skip to content
Snippets Groups Projects
Commit 195c8282 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add tests for `simpl` on `last`.

parent e1e8316a
No related branches found
No related tags found
1 merge request!277Misc improvements to `head` and `tail` functions for lists
Pipeline #48530 passed
1 goal
============================
None = None
1 goal
============================
Some 10 = Some 10
1 goal
============================
Some 11 = Some 11
1 goal
l : list nat
============================
last (11 :: l) = last (11 :: l)
1 goal
l : list nat
============================
last (10 :: l) = last (10 :: l)
From stdpp Require Import list.
Lemma last_simpl_test_nil : last [] =@{option nat} None.
Proof. simpl. Show. done. Qed.
Lemma last_simpl_test_singleton : last [10] = Some 10.
Proof. simpl. Show. done. Qed.
Lemma last_simpl_test_double : last [10; 11] = Some 11.
Proof. simpl. Show. done. Qed.
Lemma last_simpl_test_cons_cons l : last (10 :: 11 :: l) = last (11 :: l).
Proof. simpl. Show. done. Qed.
(* The following should not [simpl] and result in a [match]. *)
Lemma last_simpl_test_cons l : last (10 :: l) = last (10 :: l).
Proof. simpl. Show. done. Qed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment