How to create an instance of TotalBLE

Question

I am trying to create an instance of TotalBLE for my comparison function.

import Std.Classes.Order

-- BEGIN: no need to read, it is just here for completion sake

inductive Desc where
  | intro
    (name : String)
    (hash : UInt64)
    (params : List Desc)
    (reader: Bool)
  : Desc
  deriving Repr

def cmp (x y: Desc): Ordering :=
  match x with
  | ⟨xname, xhash, xparams, _⟩ =>
    match y with
    | ⟨yname, yhash, yparams, _⟩ =>
      let chash := compare xhash yhash
      if chash != Ordering.eq
      then chash
      else
        let cname := compare xname yname
        if cname != Ordering.eq
        then cname
        else cmps xparams yparams
where cmps (xs ys : List Desc) : Ordering :=
  match xs, ys with
  | x::xs, y::ys =>
    let r := cmp x y
    if r != Ordering.eq
    then r
    else cmps xs ys
  | _, _ => Ordering.eq

instance : Hashable Desc where
  hash x := get_hash x

instance : Ord Desc where
  compare x y := cmp x y

def le (x y: Desc): Bool :=
  match cmp x y with
  | Ordering.lt => true
  | Ordering.eq => true
  | _ => false

-- END: no need to read, it is just here for completion sake

theorem le_total: ∀ (x y: Desc),
  le x y ∨ le y x = true := by
  sorry

instance : Std.TotalBLE le where
  total x y := le_total x y

But I get a type error

type mismatch
  fun x y => le_total x y
has type
  ∀ (x y : Desc), le x y = true ∨ le y x = true : Prop
but is expected to have type
  le a✝ b✝ = true ∨ le b✝ a✝ = true : Prop
the following variables have been introduced by the implicit lambda feature
  a✝ : Desc
  b✝ : Desc
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.Lean 4

I have tried writing

instance : Std.TotalBLE le where
  @total x y := le_total x y

But then I get a syntax error

Does anyone have any ideas of how to write the syntax, so that I can work on the proof later?

Note: this is not an ask to write the proof.

Answer 1

I agree this is strange (possibly even a bug I'm not sure) but this works:

instance : Std.TotalBLE le where
  total := le_total _ _

Answer 2

I don't know why it wasn't working before, but now I am able to create those instances consistently

theorem le_total : ∀ (x y: Desc),
  le x y = true ∨ le y x = true := by
  sorry

instance : Std.TotalBLE le where
  total x y := le_total x y

theorem cmp_trans : ∀ {x y z: Desc},
  cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt := by
  sorry

instance : Std.TransCmp cmp where
  le_trans cxy cyz := cmp_trans cxy cyz
```