orelse nontermination

Stream: general

[Seul Baek]

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]

you can eta expand foo on the right

[Gabriel Ebner]

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

[Seul Baek]

@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]

@Gabriel Ebner That works. Thanks!

[Mario Carneiro]

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