DecidableRel on structures

Stream: Is there code for X?

[Bhakti Shah]

Is there something that says decLt a.f₀ b.f₀ ∧ decLt a.f₁ b.f₁ → decLt a b if a and b are structures with fields f₀ and f₁? (I'm also not sure if this is even true; but it seems true to me :D)

[Eric Wieser]

That doesn't typecheck, docs#DecidableRel takes just one argument

[Bhakti Shah]

oops I edited the question (also changed it to be a bit more specific)

[Julian Berman]

What's decLt? Can you include your imports?

[Julian Berman]

(And if it exists it probably will be with \to rather than \and, and maybe some exting)

[Bhakti Shah]

Don't have any imports. decLt as seen here, basically just a -> b -> Decidable (a < b) Here's an mwe of what i was trying to do:

abbrev ID := String

structure Name where
  id : ID
  path : List ID

deriving instance DecidableEq for Name

instance : LT Name where
  lt a b := (a.id < b.id) ∧ (a.path < b.path)

instance Name.decLt (n m : Name) : Decidable (n < m)  := sorry

[Eric Wieser]

Note your edited version still doesn't typecheck (assuming it refers to String.decLt), as decLt is a proof not a proposition

[Eric Wieser]

Your new version is fine, but it doesn't resemble your question any more!

[Eric Wieser]

instance Name.decLt (n m : Name) : Decidable (n < m)  := by
  show Decidable (_ ∧ _)
  infer_instance

[Eric Wieser]

Or even use docs#instDecidableAnd directly:

instance Name.decLt (n m : Name) : Decidable (n < m) := instDecidableAnd

[Bhakti Shah]

oh that's amazing thank you! sorry about the original question i keep trying to generalize my question :')