function expected at ?

Stream: new members

[Lucas Viana]

On the last line of this #mwe, a is of type M → M. But then lean complains it has type m_1 and is not a function! why is that? :anguished:

import group_theory.subgroup
open function
variables (M : Type*)

instance endo_monoid : monoid (M → M) := begin
  fapply monoid.mk,
  use comp,
  intros, refl,
  use id,
  intro, refl,
  intro, refl,
end
instance endo_hasid : has_one (M → M) := by apply_instance
instance endo_semigroup : semigroup (M → M) := by apply_instance

definition dynamical_system := submonoid (M → M)

instance dyn_mem : has_mem (M → M) (dynamical_system M) := submonoid.has_mem

def orbit (x : M) (dyn : dynamical_system M) :=
{p : M | ∃(a : M → M) (a ∈ dyn), p = a x} -- ??

[Johan Commelin]

You want (h : a \in dyn).

[Johan Commelin]

Also, if you didn't use a as variable, you would have gotten a more useful error message.

[Johan Commelin]

This is a very frustrating bug... the a-bug.

[Johan Commelin]

With a bit of luck, this would also do what you want:

def orbit (x : M) (dyn : dynamical_system M) :=
{p : M | ∃ f ∈ dyn, p = f x}

[Lucas Viana]

so I always need to name my hypothesis when writing "exists..."?

[Johan Commelin]

(I didn't test it.)

[Johan Commelin]

In your initial code, change the a to f, and then look at the tactic state before the error message...

[Lucas Viana]

your last example does not work (I tried it before)

[Johan Commelin]

You will see that there are two fs and an a.

[Reid Barton]

I don't think it's the a bug here--it would be the H bug.

[Johan Commelin]

Ok, too bad... if the short versions don't work, then you need to give more names (-;

[Lucas Viana]

ok, thank you :slight_smile: we could have a list of those strange bugs and their common symptoms