Zulip Chat Archive

Stream: general

Topic: Strange term creation error


Bhavik Mehta (May 11 2020 at 15:29):

MWE:

import category_theory.types
import category_theory.monad.basic

open category_theory monad

@[simps]
def P : Type  Type :=
{ obj := λ X, set X,
  map := λ X Y, set.image }

def P_monad : monad P :=
{ η :=
  { app := λ Y x, ({x} : set Y),
    naturality' := by tidy },
  μ :=
  { app := λ Y x, set.sUnion x,
    naturality' := by tidy },
  left_unit' := by tidy,
  right_unit' := by tidy,
  assoc' := by tidy }

Each of the tidy seem to succeed, but the monad structure gives me this error:

type mismatch at application
  a_h_left_w a
term
  a
has type
  X_1
but is expected to have type
  X
types contain aliased name(s): X
remark: the tactic `dedup` can be used to rename aliases

Bhavik Mehta (May 11 2020 at 15:30):

Is something strange happening inside the tidy?

Bhavik Mehta (May 11 2020 at 15:31):

Replacing the tidy with the tactic script tidy? tells me gives the same error

Markus Himmel (May 11 2020 at 15:33):

Maybe it's https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20and.20dedup again?

Bhavik Mehta (May 11 2020 at 15:35):

Yeah that seems like the same problem

Reid Barton (May 15 2020 at 22:50):

I also just encountered this.

Bhavik Mehta (May 15 2020 at 22:52):

I think it should be fixed here: https://github.com/leanprover-community/lean/issues/236


Last updated: Dec 20 2023 at 11:08 UTC