feat: translate comments

[gebner]

This works by annotating the translated Syntax objects with synthetic positions from the Lean 3 source file (using 10000*line+column as the string position). The trExpr function therefore now takes an argument of type Spanned Expr instead of Expr and implicitly uses withRef so that syntax quotations add the desired range. If the resulting syntax still doesn't have a range (e.g. because it is constructed manually), then trExpr sets the info on the resulting syntax. Before the syntax is printed (but after transformations), the comments are inserted into the syntax at reasonable positions.

Fixes #101

[gebner]

Skimming through the diff here are some other issues:

1. Comments are not attached to anonymous constructors, but to the term inside. (Maybe unicode related?)

2. The line break in the comment messes up the indentation (which probably breaks parsing in some cases).

   @[to_additive]
   instance : Inhabited CommMon :=
   ⟨-- The default instance for `comm_monoid punit` is derived via `punit.comm_ring`,
       -- which breaks to_additive.
       @of
       PUnit <|
     @CommGroupₓ.toCommMonoid _ PUnit.commGroup⟩

3. Missing spaces before comments (in the Lean 3 file, the comment was also directly after calc).

   · calc-- non-terminating case
           (0 : K) ≤
           fib (n + 1) :=
         by
          exact_mod_cast (n + 1).fib.zero_le _ ≤ ((of v).continuantsAux (n + 1)).b :=

4. Not sure what's going on here, the comments were originally after the = and the <|:

   private theorem mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c) := by
   suffices
   (-- `λ a b c, a * b * c` as a bundled hom
             mulHom
             A).compHom.comp
       (mulHom A) =
     (AddMonoidHom.compHom flipHom <|
         (-- `λ a b c, a * (b * c)` as a bundled hom
                   mulHom
                   A).flip.compHom.comp
           (mulHom A)).flip
   from AddMonoidHom.congr_fun (AddMonoidHom.congr_fun (AddMonoidHom.congr_fun this a) b) c