20 lines
966 B
Text
20 lines
966 B
Text
id : Π {A}, A → A
|
|
id₂ : Π {A}, A → A
|
|
foo1 : A → B → A
|
|
foo2 : A → B → A
|
|
foo3 : A → B → A
|
|
foo4 : A → B → A
|
|
foo1 : Π {A} {B}, A → B → A
|
|
foo2 : Π {A} B, A → B → A
|
|
foo3 : Π A {B}, A → B → A
|
|
foo4 : Π A B, A → B → A
|
|
boo1 : Π {A} {B}, A → B → A
|
|
boo2 : Π {A} B, A → B → A
|
|
boo3 : Π A {B}, A → B → A
|
|
boo4 : Π A B, A → B → A
|
|
param_binder_update.lean:70:12: error: invalid parameter binder type update, 'A' is a variable
|
|
param_binder_update.lean:71:11: error: invalid variable binder type update, 'C' is not a variable
|
|
param_binder_update.lean:72:12: error: invalid variable binder type update, 'C' is not a variable
|
|
param_binder_update.lean:73:12: error: invalid variable binder type update, 'C' is not a variable
|
|
param_binder_update.lean:77:12: error: invalid parameter binder type update, 'id3' is not a parameter
|
|
param_binder_update.lean:81:12: error: invalid variable binder type update, 'C' is not a variable
|