diff options
| author | Pierre-Marie Pédrot | 2017-08-24 17:14:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-24 17:15:48 +0200 |
| commit | c515a8acb4acbe7e73121f1060ffef31d96a1436 (patch) | |
| tree | a99277a77c26e3cafa33556fbbecd916d4ec0fe3 /tests/example2.v | |
| parent | 60a98c8092a0293b852712f8e21ead6e0ef1e064 (diff) | |
Adding a notation for the unfold tactic.
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index af664ef163..6b26b78022 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -182,3 +182,11 @@ Proof. lazy. reflexivity. Qed. + +Goal let x := 1 + 1 - 1 in x = x. +Proof. +intros x. +unfold &x at 1. +let x := reference:(Nat.sub) in unfold Nat.add, $x in x. +reflexivity. +Qed. |