blob: 8e1010767342cd7880cf787f02b6b29f5225e55d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
The command has indeed failed with message:
In environment
list' : Set -> Set
A : Set
a : A
l : list' A
Unable to unify "list' (A * A)%type" with "list' A".
Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x
Arguments foo _%type_scope _
Arguments Foo _%type_scope _
myprod unit bool
: Set
|
