diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/change.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v index cea017122e..c72ee875af 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -4,3 +4,9 @@ Goal let a := 0+0 in a=a. intro. change 0 in (value of a). change ((fun A:Type => A) nat) in (type of a). +Abort. + +Goal forall x, 2 + S x = 1 + S x. +intro. +change (?u + S x) with (S (u + x)). +Abort. |