search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

Notations no longer work in binport #192

Open gebner opened 2 years ago

gebner commented 2 years ago

Like ≅+* or ℝ

gebner commented 2 years ago

Oof, I think this is an ugly error...

When we elaborate the Lean 4 notation command, we get this:

/- sources/mathlib/src/data/real/basic.lean:1:270000: error: application type mismatch
  Lean.withRef f✝
argument
  f✝
has type
  Lean.TSyntax `ident : Type
but is expected to have type
  Lean.Syntax : Type
 -/

Apparently we get an exception during TC synthesis (but it's not timeout related from what I can tell), not even this works:

#check fun n : Nat => (n : Option Nat)
gebner commented 2 years ago

Apparently, this instance is dangerous now:

@DirectSum.GradeZero.nonUnitalNonAssocSemiring :
{ι : Type ?u.302} →
  [_inst_1 : DecidableEq ι] →
    (A : ι → Type ?u.303) →
      [_inst_2 : AddZeroClass ι] →
        [_inst_3 : (i : ι) → AddCommMonoid (A i)] →
          [_inst_4 : DirectSum.GnonUnitalNonAssocSemiring A] →
            NonUnitalNonAssocSemiring (A Zero.zero)

What happens is that we try e.g. unifying NonUnitalNonAssocSemiring (Option ℕ) ≟ NonUnitalNonAssocSemiring (?m.306 Zero.zero). But then the defeq module throws an isDefEqStuck exception aborting the whole TC synthesis.

gebner commented 2 years ago

Changing Zero.zero to 0 didn't help. 😢

gebner commented 2 years ago

Maybe after the discrimination tree refactor where we no longer do iota-reduction. (Right now 0 is binported as @ofNat ι 0 { ofNat := Zero.zero }.)