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

bad interaction between `mod_cases` and `induction` #1851

Closed

dwrensha opened this issue Jan 26, 2023 · 0 comments

Member

dwrensha commented Jan 26, 2023

This code gives me an unexpected error:

import Mathlib.Tactic.ModCases

theorem foo (n : ℕ) (z : ℤ) : n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
     mod_cases z % 3
     · sorry
     · sorry
     · sorry

/-
type mismatch
  sorryAx ?m.55
has type
  ?m.55 : Sort ?u.54
but is expected to have type
   Nat.succ _uniq.37 = Nat.succ _uniq.37 : Prop
-/

dwrensha mentioned this issue

[Merged by Bors] - fix: set the local context in mod_cases #1865

Closed

bors bot closed this as completed in

9a20112

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment