blob: fe537c59a783b40b304b12c185adb0ce97525437 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* Check that types are not uselessly unfolded *)
(* Check here that P returns something of type "option L" and not
"option (list nat)" *)
Definition L := list nat.
Definition P (e:option L) :=
match e with
| None => None
| Some cl => Some cl
end.
Print P.
(* Check that plus is folded even if reduction is involved *)
Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
|
