blob: 51b8e618a130625c4883b7b3ae43f0533226cfc3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(* error 2 *)
Goal (exists f: Set -> nat, f nat = 0).
Proof. set (f:= fun _:Set =>0). by exists f. Qed.
Goal (exists f: Set -> nat, f nat = 0).
Proof. set f := (fun _:Set =>0). by exists f. Qed.
|
