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