Zulip Chat Archive

Stream: general

Topic: type_of and friends


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 12 2019 at 07:05):

I would suggest using meta code for best results

view this post on Zulip Johan Commelin (Nov 12 2019 at 07:07):

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

view this post on Zulip 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