## Stream: general

### Topic: type_of and friends

#### Johan Commelin (Nov 12 2019 at 06:44):

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 (Nov 12 2019 at 07:05):

I would suggest using meta code for best results

#### Johan Commelin (Nov 12 2019 at 07:07):

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

#### Johan Commelin (Nov 12 2019 at 07:07):

I'll try to figure this out myself

Last updated: May 10 2021 at 18:22 UTC