showing implicit type conversions

Stream: lean4

[Kayla Thomas]

Is there a way to highlight instances of or turn off implicit type conversions? For example, the v = x in the forall_ case here that I think is being implicitly converted from a Prop to a Bool?

def isBoundIn (v : VarName) : Formula → Bool
  | true_ => false
  | pred_ _ _ => false
  | not_ phi => isBoundIn v phi
  | imp_ phi psi => isBoundIn v phi || isBoundIn v psi
  | forall_ x phi => v = x || isBoundIn v phi

[Damiano Testa]

Does using == work? This should be the notation for Boolean equality: docs4#BEq.

[Kayla Thomas]

Both = and == type check fine. I'm sorry, I didn't mean to ask how to fix it, but for a way to highlight implicit coercions in cases like this so that I was better aware that I should have put == there instead of =.

[Damiano Testa]

I do not know if there is a pp-option to highlight this somehow in the infoview. This is something that often works for me:

def f : Bool := 0 = 0
def g : Bool := 0 == 0

#print f  -- def f : Bool := decide (0 = 0)
#print g  -- def g : Bool := 0 == 0

The presence of decide highlights that Lean is doing some work to convert the Prop to a Bool.

[Kayla Thomas]

Thank you. An option to turn off the implicit conversion might work too. Then I would get an error.

[Damiano Testa]

I do not know how to do this programmatically, but I suspect that you have a DecidableEq on VarName, maybe? Disabling that should error on equalities, at least. Here is an example:

attribute [-instance] instDecidableEqNat

def f (n : Nat): Bool := n = n  -- type mismatch
def g : Bool := 0 == 0

[Kayla Thomas]

Interesting. Thank you.

[Damiano Testa]

I feel that this is only useful after the fact: you should already be aware of which decidable instance you have. I am not sure how to cripple decide, nor whether there is also something else that might need disabling... :man_shrugging: