Stream: MetaCoq

Topic: tmTry


view this post on Zulip Jason Gross (Mar 26 2023 at 03:06):

Would it be reasonable to get a tmTry in the template monad? I want to be able to try tmAxiom, tmDefinition, tmUnquote, and tmUnquoteTyped and have the option to try something different if these fail with a universe inconsistency

view this post on Zulip Théo Winterhalter (Mar 26 2023 at 19:40):

I guess you want something more than an equivalent of try from LTac but something that also tells you wether it succeeded or not? Something like tmTry : TM a -> TM (option a)? I guess it would much more work to also reify the errors themselves.

view this post on Zulip Jason Gross (Mar 26 2023 at 19:55):

Yes, tmTry : TM a -> TM (option a) would be great. I don't need reification of errors, though I guess that'd be the most general thing.

view this post on Zulip Jason Gross (Mar 26 2023 at 19:58):

Presumably a more forward-compatible solution would be Inductive result a := Val (_ : a) | Err (_ : exn). with Variant exn := EUnknown. or something for now, with the option to extend the reification of errors in the future without having to modify code that uses tmTry too much.

view this post on Zulip Jason Gross (Mar 26 2023 at 20:47):

I've made a feature request issue at https://github.com/MetaCoq/metacoq/issues/874. How hard would this be to implement?


Last updated: Jul 23 2024 at 20:01 UTC