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