Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

fix(tactic/norm_num) Bugfix for norm num when testing divisibility of integers#2355

Merged
mergify[bot] merged 2 commits intomasterfrom
norm-num-int-dvd
Apr 9, 2020
Merged

fix(tactic/norm_num) Bugfix for norm num when testing divisibility of integers#2355
mergify[bot] merged 2 commits intomasterfrom
norm-num-int-dvd

Conversation

@alexjbest
Copy link
Copy Markdown
Member

They were assumed nats somehow leading to

example (h : (5 : ℤ) ∣ 2) : false := by norm_num at h

giving

type mismatch at application
  has_mod.mod 2
term
  2
has type
  ℤ
but is expected to have type
  ℕ

TO CONTRIBUTORS:

Make sure you have:

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

@alexjbest alexjbest changed the title Bugfix for norm num when testing divisibility of integers fix(tactic/norm_num) Bugfix for norm num when testing divisibility of integers Apr 8, 2020
@alexjbest alexjbest added the awaiting-review The author would like community review of the PR label Apr 8, 2020
@digama0 digama0 added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 8, 2020
@mergify mergify bot merged commit e4e483e into master Apr 9, 2020
@mergify mergify bot deleted the norm-num-int-dvd branch April 9, 2020 00:01
butterthebuddha pushed a commit to butterthebuddha/mathlib that referenced this pull request May 15, 2020
…-community#2355)

they were assumed nats somehow

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
butterthebuddha pushed a commit to butterthebuddha/mathlib that referenced this pull request May 16, 2020
…-community#2355)

they were assumed nats somehow

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
…-community#2355)

they were assumed nats somehow

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants