type_of and friends

Stream: general

[Johan Commelin]

I can make the following definitions:

variables {X : Type*} {x y : X}

def type_of (x : X) := X

def eq.LHS (h : x = y) := x
def eq.RHS (h : x = y) := y

def iff.LHS {P Q : Prop} (h : P ↔ Q) := P
-- etc

But these definitions are not very transparent. I can make them abbreviations which might be a bit better. But would it be possible to define them in such a way that they are completely transparent to the pretty printer? Or do I need to turn to meta code here?

[Mario Carneiro]

I would suggest using meta code for best results

[Johan Commelin]

Ok... that gives me another chance to level-up my Lean-proving skills (-;

[Johan Commelin]

I'll try to figure this out myself