blob: 6366130cbd0f1b010d76afd779926533e93e8031 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* (c) Copyright 2006-2016 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.
|
