## Stream: general

### Topic: orelse nontermination

#### Seul Baek (Dec 26 2018 at 05:58):

meta def foo : tactic unit :=
triv <|> foo

example : true := by foo


In this example I expected foo to behave just like triv since the right branch would never be used, but it times out. Is there a way to avoid this?

#### Mario Carneiro (Dec 26 2018 at 06:58):

you can eta expand foo on the right

#### Gabriel Ebner (Dec 26 2018 at 08:19):

Another nice option is to use local attribute [inline] interaction_monad_orelse.

#### Seul Baek (Dec 26 2018 at 12:15):

@Mario Carneiro I thought you meant changing the body of foo to triv <|> (λ s, foo s), but this still times out. Am I doing something wrong here?

#### Seul Baek (Dec 26 2018 at 12:17):

@Gabriel Ebner That works. Thanks!

#### Mario Carneiro (Dec 26 2018 at 20:07):

actually I think you have to eta expand the definition of foo itself, i.e. def foo | s := (triv <|> foo) s

Last updated: May 14 2021 at 12:18 UTC