aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/change.v
blob: cea017122e9d1ca60201c56895eb6a14a3b335a7 (plain)
1
2
3
4
5
6
(* A few tests of the syntax of clauses and of the interpretation of change *)

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).