blob: f00434622c5ad4f7fae0b72b63ad195b8ae4c30d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import 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.
|
