## Stream: Is there code for X?

### Topic: a mutable tactic

#### Kenny Lau (May 16 2020 at 07:42):

is it possible to write a tactic:

meta def increment : tactic unit :=


such that every time I do #eval by increment it prints 0 and then 1 and then 2 etc?

#### Kenny Lau (May 16 2020 at 07:42):

#eval by increment -- 0
#eval by increment -- 1
#eval by increment -- 2


#### Kenny Lau (May 16 2020 at 07:43):

I imagine I could start by inspect how random works

#### Kenny Lau (May 16 2020 at 07:44):

this behaviour is also acceptable:

#eval by {increment, increment, increment} -- 0 \n 1 \n 2


#### Kenny Lau (May 16 2020 at 07:47):

Kenny Lau said:

I imagine I could start by inspect how random works

welp I'm out of luck as I've hit the constant wall

#### Kenny Lau (May 16 2020 at 07:48):

I imagine I could also use the help of an outside file, if I've resolved the issue of not being able to open files

#### Kenny Lau (May 16 2020 at 07:56):

it doesn't have to go on forever, e.g. by reading a file that basically contains 0\n1\n2\n3\n4

#### Kenny Lau (May 16 2020 at 07:56):

then it's basically "read the next line" tactic

#### Gabriel Ebner (May 16 2020 at 08:40):

You could use user_attribute to set (and modify) an attribute on the increment declaration.

#### Mario Carneiro (May 16 2020 at 08:47):

is there an approach with less performance cost than this? Particularly when the object being stored is large

#### Kenny Lau (May 16 2020 at 09:58):

meta def hack : list expr :=
[(42), (57)]

@[user_attribute]
meta def incr_attr : user_attribute unit ℕ :=
{ name   := incrementer,
descr  := "incrementer",
parser := pure 0 }

open tactic
meta def increment : tactic unit :=
do n ← incr_attr.get_param increment <|> pure 0,
e ← hack.nth (n % 2),
tactic.exact e,
incr_attr.set increment (n+1) tt

def test0 : ℕ := by increment
def test1 : ℕ := by increment
def test2 : ℕ := by increment
def test3 : ℕ := by increment
#print test0 -- 42
#print test1 -- 57
#print test2 -- 42
#print test3 -- 57


#### Kenny Lau (May 16 2020 at 09:58):

this works perfectly

thanks to Mario

#### Kenny Lau (May 16 2020 at 10:07):

@Mario Carneiro is there a way to change the environment permanently?

#### Kenny Lau (May 16 2020 at 10:07):

this doesn't survive <|>

#### Kenny Lau (May 16 2020 at 10:09):

lemma test : true :=
by rw [by increment] <|> rw [by increment] <|> rw [by increment]


#### Kenny Lau (May 16 2020 at 10:09):

this just gives 3 zeroes

#### Kenny Lau (May 16 2020 at 10:10):

maybe we really need to do some read/write?

#### Kenny Lau (May 16 2020 at 10:11):

but then we would need some way to pass from io to tactic

#### Markus Himmel (May 16 2020 at 11:21):

Kenny Lau said:

but then we would need some way to pass from io to tactic

Like tactic.unsafe_run_io`?

#### Kenny Lau (May 16 2020 at 12:09):

seriously it takes more time to hack your kata

#### Kenny Lau (May 16 2020 at 12:09):

then is it still a hack?

Last updated: May 07 2021 at 21:10 UTC