# Zulip Chat Archive

## Stream: new members

### Topic: Reflexive product order

#### YurySerdyuk (Jun 29 2023 at 15:43):

What is wrong with the syntax of my code :

@[class] structure refl_order (A : Type) extends has_le A :=

(refl : ∀ a, le a a)

def prod_order {A B : Type} (o₁ : A → A → Prop) (o₂ : B → B → Prop) (s : A × B) (t : A × B) :=

o₁ (s.1) (t.1) ∧ o₂ (s.2) (t.2)

instance refl_prod {A B: Type} [o₁ : refl_order A] [o₂ : refl_order B] : refl_order (A × B) :=

let op : A × B → A × B → Prop := prod_order o₁.le o₂.le in

have refl : ∀ p : A × B, op p p, by intro; apply and.intro; repeat {apply refl_order.refl},

show _, from refl_order.mk (has_le.mk op) refl

type mismatch at application

{to_has_le := ?m_2, refl := {le := op}}

term

{le := op}

has type

has_le (A × B) : Type

but is expected to have type

∀ (a : ?m_1), a ≤ a : Prop

error message

too many arguments

#### Bolton Bailey (Jun 29 2023 at 16:03):

Here is the code with #backticks

```
@[class] structure refl_order (A : Type) extends has_le A :=
(refl : ∀ a, le a a)
def prod_order {A B : Type} (o₁ : A → A → Prop) (o₂ : B → B → Prop) (s : A × B) (t : A × B) :=
o₁ (s.1) (t.1) ∧ o₂ (s.2) (t.2)
instance refl_prod {A B: Type} [o₁ : refl_order A] [o₂ : refl_order B] : refl_order (A × B) :=
let op : A × B → A × B → Prop := prod_order o₁.le o₂.le in
have refl : ∀ p : A × B, op p p, by intro; apply and.intro; repeat {apply refl_order.refl},
show _, from refl_order.mk (has_le.mk op) refl
```

#### Bolton Bailey (Jun 29 2023 at 16:08):

It seems `refl_order.mk`

is supposed to only have one explicit argument, of type `(∀ (a : A), a ≤ a)`

, but this code gives two arguments, `(has_le.mk op)`

and `refl`

#### Bolton Bailey (Jun 29 2023 at 16:10):

I see the issue - you included the `(has_le.mk op)`

as one of the arguments, but this was supposed to be implicit, so Lean got confused.

#### Bolton Bailey (Jun 29 2023 at 16:11):

This fixes it `@refl_order.mk _ (has_le.mk op) refl`

. The `@`

tells Lean to treat all implicit arguments as explicit, after which there are three arguments, and the `_`

tells Lean to infer the first one.

#### Bolton Bailey (Jun 29 2023 at 16:14):

@YurySerdyuk

Last updated: Dec 20 2023 at 11:08 UTC