blob: fc3b6fbd9938fff88466d4e2c5697181000cf59d (
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
|
