blob: 2a8850288c1eab755b393dfce04c9936089e9043 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import seq.
Lemma test1 : True.
have f of seq nat & nat : nat.
exact 3.
have g of nat := 3.
have h of nat : nat := 3.
have _ : f [::] 3 = g 3 + h 4.
Admitted.
|
