## Stream: new members

### Topic: use in tactic

#### Angela Li (Dec 31 2020 at 05:17):

Hello! I'm trying to make Fifteen. Here is hopefully a MWE leanproject get SnobbyDragon/leanfifteen && code leanfifteen (https://github.com/SnobbyDragon/leanfifteen)

In the fifteentactics.lean file, my slide_tile tactic is failing when I try to use the use tactic. I think it's parallel to this problem:

import tactic

meta def solve (n : ℕ) : tactic unit :=
do [use n] <|> tactic.fail ":("

example : ∃ n : ℕ, n + 1 = 2 :=
begin
solve 1,
end


This fails but works if I do [use 1]. Is there a way to fix this?
Thanks!

what is Fifteen?

#### Mario Carneiro (Dec 31 2020 at 05:25):

oh this is the 4x4 sliding puzzle?

yeet

I guess so

#### Mario Carneiro (Dec 31 2020 at 05:26):

You are passing the literal n to the use tactic there

#### Angela Li (Dec 31 2020 at 05:28):

uhhh I think I don't know what that means

#### Mario Carneiro (Dec 31 2020 at 05:29):

import tactic

namespace tactic
namespace interactive
setup_tactic_parser
meta def solve (n : parse texpr) : tactic unit :=
do use [n] <|> tactic.fail ":("
end interactive
end tactic

example : ∃ n : ℕ, n + 1 = 2 :=
begin
solve 1,
end


#### Mario Carneiro (Dec 31 2020 at 05:30):

the previous version was doing basically solve 1 = use n and it would complain that n doesn't exist at the point of use

#### Mario Carneiro (Dec 31 2020 at 05:30):

and the n : nat was unused

#### Angela Li (Dec 31 2020 at 05:30):

Ohhhh okay that makes sense. Ahhhh parsing I haven't done that yet. time to learn something new. thanks!

#### Mario Carneiro (Dec 31 2020 at 05:31):

alternatively, without the fancy parser, closer to your original version:

import tactic

meta def solve (n : ℕ) : tactic unit :=
do tactic.interactive.use [pexpr.of_expr (reflect n)] <|> tactic.fail ":("

example : ∃ n : ℕ, n + 1 = 2 :=
begin
solve 1,
end


#### Mario Carneiro (Dec 31 2020 at 05:33):

we have to turn n : nat back into a pexpr because that's what use takes as input

#### Angela Li (Dec 31 2020 at 05:33):

Okay thanks! I will try this on tiles now :)

#### Mario Carneiro (Dec 31 2020 at 05:34):

remember that tactics deal in exprs, not the actual types that you see at the user level. This allows them to do some things that would otherwise be impossible, but requires you to get your head around all the parsing and quoting and antiquoting stuff

Last updated: May 14 2021 at 21:11 UTC