Zulip Chat Archive

Stream: new members

Topic: Problems with meta variable in goal


view this post on Zulip Eric Mark Martin (Dec 06 2019 at 09:05):

Hey, I’m new to lean but having some trouble where an exact I’m providing won’t unify because the goal has a metavariable in it

view this post on Zulip Johan Commelin (Dec 06 2019 at 09:06):

Could you provide a minimal (non-)working example (MWE), please?

view this post on Zulip Johan Commelin (Dec 06 2019 at 09:07):

As in, copy-paste your code

```lean
code goes here (you get syntax-highlighting!)
```

view this post on Zulip Johan Commelin (Dec 06 2019 at 09:07):

That will make it a lot easier for us to help you

view this post on Zulip Johan Commelin (Dec 06 2019 at 09:07):

Also: welcome :wink:

view this post on Zulip Eric Mark Martin (Dec 06 2019 at 09:22):

Thank so much—I’m actually having a lot of trouble getting a mwe which is part of the difficulty—I can’t tell why it lets me do what I want sometimes but not here

view this post on Zulip Eric Mark Martin (Dec 06 2019 at 09:23):

The proof is actually for a class so I don’t want to paste it here online

view this post on Zulip Eric Mark Martin (Dec 06 2019 at 09:27):

I think the error message that captures the gist of the issue though is

invalid apply tactic, failed to unify
  Expr.Num x ~ Expr.Num ?m_1
with
  ?m_2 ~ ?m_2

view this post on Zulip Eric Mark Martin (Dec 06 2019 at 09:28):

Where Expr.num x ~ Expr.Num ?m_1 is my goal as a result of an existential introduction

view this post on Zulip Kevin Buzzard (Dec 06 2019 at 10:21):

If you're not going to post any code it's difficult to help. Try explicitly writing some type ascriptions in some clever places (ie write (_ : nat) instead of _) and see if it helps

view this post on Zulip Kevin Buzzard (Dec 06 2019 at 10:22):

Maybe the elaborater is doing things in a silly order and needs some hints


Last updated: May 15 2021 at 00:39 UTC