Data.Rat.MetaDefs

Stream: mathlib4

[Jihoon Hyun]

I;m trying to port Data.Rat.MetaDefs. I could find the expr is defined in the lean3 standard. What is the alternative of that in lean4?

[Eric Wieser]

docs4#Lean.Expr

[Eric Wieser]

Didn't mathport answer that for you though?

[Mario Carneiro]

No, meta code has very few alignments because we aren't using mathport to port meta code

[Mario Carneiro]

I think it is reasonable to have a few obvious alignments like expr, level, name though

[Eric Wieser]

Yeah, I think we may as well put in the obvious alignments to get people started

[Jeremy Tan]

Would the ported file indeed lie at Mathlib/Data/Rat/MetaDefs.lean or would it go somewhere else?

[Scott Morrison]

It's a moot point, this is a meta file and if it needs porting / replacing for some concrete purpose in other meta code, then the authors of that will presumably decide where the material goes. We're simply not porting meta code on a "file-by-file" basis.

[Thomas Murrills]

We seem to be porting this now on #5934; I noticed it on #help-wanted. Many or all of these defs seem to overlap with internal norm_num components. Should we refactor them to use those internal norm_num components? Or are we porting this file separately as a demonstration of Qq, or for some other reason? (Sorry, I couldn't find a recent zulip discussion about this file, though I thought I saw one somewhere...)

[Eric Wieser]

I just thought I'd have a go at porting it as a Qq exercise

[Eric Wieser]

I agree there's almost certainly overlap

[Eric Wieser]

I think the defs that are probably actually useful are:

• def Qq.ofRat {u : Lean.Level} (α : Q(Type u)) : ℚ → Lean.MetaM Q($α)
• def Rat.toExprQ {u : Lean.Level} (α : Q(Type u)) (_ : Q(Neg $α)) (_ : Q(Div $α)) (q : ℚ) (_ : let qnna := q.num.natAbs; by exact Q(OfNat $α $qnna)) (i3 : let qd := q.den; by exact Q(OfNat $α $qd)) : Q($α)