# How to create an instance of TotalBLE

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)
: 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.

• Btw I have the same issue with Std.TransCmp Mar 10, 2023 at 15:43

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

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

• Yeah it does feel like a bug, but this works until it is fixed, thank you :) Mar 12, 2023 at 11:34
• In the end I got the following to work  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: Desc), cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt := by sorry instance : Std.TransCmp cmp where le_trans := cmp_trans _ _  I do think there is a bug Mar 12, 2023 at 11:41

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
$$$$
`