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.