Zulip Chat Archive

Stream: general

Topic: induction bug


view this post on Zulip Kenny Lau (Nov 20 2018 at 22:46):

theorem wtf {α : Type u} (C : multiset α  Prop) (r) : C r :=
begin
  induction r using multiset.induction
  /-
2 goals
case h₁
α : Type u,
C : multiset α → Prop
⊢ C 0

case h₂
α : Type u,
C : multiset α → Prop,
r_a : list α,
r_s : multiset (list α),
r_a_1 : C r_s
⊢ C (r_a :: r_s)
  -/,
  sorry, sorry
end

/-
type mismatch at application
  @multiset.induction (list α)
term
  list α
has type
  Type u
but is expected to have type
  Type (u+1)
-/

Last updated: May 15 2021 at 22:14 UTC