Zulip Chat Archive

Stream: general

Topic: orelse nontermination


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Dec 26 2018 at 06:58):

you can eta expand foo on the right

view this post on Zulip Gabriel Ebner (Dec 26 2018 at 08:19):

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

view this post on Zulip 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?

view this post on Zulip Seul Baek (Dec 26 2018 at 12:17):

@Gabriel Ebner That works. Thanks!

view this post on Zulip 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