Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Notations no longer work in binport #192

Open
gebner opened this issue Oct 26, 2022 · 4 comments · Fixed by #196
Open

Notations no longer work in binport #192

gebner opened this issue Oct 26, 2022 · 4 comments · Fixed by #196

Comments

@gebner
Copy link
Member

gebner commented Oct 26, 2022 •
edited
Loading

Like ≅+* or ℝ
@gebner
Copy link
Member Author

gebner commented Oct 28, 2022

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
Copy link
Member Author

gebner commented Oct 28, 2022

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 gebner mentioned this issue Nov 1, 2022
Merged
@gebner gebner reopened this Nov 16, 2022
@gebner
Copy link
Member Author

gebner commented Nov 16, 2022

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

@gebner
Copy link
Member Author

gebner commented Nov 16, 2022

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

@digama0 digama0 mentioned this issue Nov 17, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this issue Nov 17, 2022
@digama0
chore: cleanup for mathport update (#620)
bf8af5f 
* `add_decl_doc` already exists in core (this declaration was just shadowing it)
* `setup_tactic_parser` is not planned for porting; the nearest equivalent is nothing at all
* `mk_simp_attribute` can mostly be aligned to `register_simp_attr`, and the remaining part (the `:= ids,*`) can't be supported at all and will give a suitable port message in mathport
* `std_next` alignment consistently gives a stack overflow when porting on my machine; I think this is a recent regression (possibly leanprover-community/mathport#192?) but this is a quick fix since this function doesn't matter too much.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Remove references to HasZero/HasOne leanprover-community/mathport
1 participant
@gebner