Inductive type Pair

Stream: lean4

[Gabriel gomez]

Hi. I'm trying to adapt the code from this paper to Lean: http://strictlypositive.org/CJ.pdf

While doing it, I'm getting a compilation error I can't understand:

inductive Pair (p q : x -> Type) (x: Type)  where
  | mk : x -> p x ->  q x -> Pair p q x

Ther error say:

Type
application type mismatch
q x
argument
x
has type
Type : Type 1
but is expected to have type
x:cross: : Sort ?u.4373Lean 4

[Gabriel gomez]

Could yoe help me understanding this. I tried with ChatGPT unsuccesfully.

[Henrik Böving]

You are referring to x in the declaration of the inductive before declaring it so the autoImplicit feature adds it as an implicit argument to yoru current type which ends up making the explicitly written out x refer to a completely different thing than the type of the argument of p and q

Don't use chatgpt to debug Lean 4 code, it has barely any clue about what is going on and will most likely produce misinformation

[Gabriel gomez]

Using this code:

  inductive Pair (x: Type) (p q : x -> Type)   where
  | mk : x -> p x ->  q x -> Pair p q x

I'm getting this error:

application type mismatch
Pair p
argument
p
has type
x → Type : Type 1
but is expected to have type
Type : Type 1

[Henrik Böving]

yes the arguments at yoru result type are mixed up now

[Gabriel gomez]

And yes, I'm getting better results with ChatGPT explaining C sharp code.

[Henrik Böving]

and then finally you probably want to write:

inductive Pair (x : Type) (p q : x -> Type)  where
  | mk : (a : x) -> p a ->  q a -> Pair x p q

something like this instead

[Gabriel gomez]

Thanks, You are exactly right. ChatGTP is very far from humans for now.