File: Reordering.v

package info (click to toggle)
coq 8.20.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: sid, trixie
  • size: 44,116 kB
  • sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2
file content (15 lines) | stat: -rw-r--r-- 379 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
 
(* Testing the reordering of hypothesis required by pattern, fold and change. *)
Goal forall (A:Set) (x:A) (A':=A), True.
intros.
fold A' in x. (* succeeds: x is moved after A' *)
Undo.
pattern A' in x.
Undo.
change A' in x.
Abort.

(* p and m should be moved before H *)
Goal forall n:nat, n=n -> forall m:nat, let p := (m,n) in True.
intros.
change n with (snd p) in H.
Abort.