Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC