Zulip Chat Archive

Stream: general

Topic: Potential vm bug


view this post on Zulip Keeley Hoek (Aug 11 2018 at 11:10):

The following code typechecks:

meta def oopsie : list string → tactic (option string)
| [] := none                          -- I'm being naughty on this line
| (a :: rest) := oopsie rest

#eval oopsie ["a"]

I don't understand why it should. If I inspect the output of the #eval, I see the output "failed". Have I found a bug in the VM?

view this post on Zulip Edward Ayers (Aug 11 2018 at 11:32):

There is a coercion from option to tactic in tactic.lean:

meta instance opt_to_tac : has_coe (option α) (tactic α) :=
returnopt

view this post on Zulip Edward Ayers (Aug 11 2018 at 11:33):

So your tactic will throw if you give it an empty list

view this post on Zulip Keeley Hoek (Aug 11 2018 at 11:36):

Ah, cheers!

view this post on Zulip Edward Ayers (Aug 11 2018 at 11:38):

I only spotted this because I happen to be reading tactic.lean currently. Does anyone know if there is a way to discover what coercions are occurring in a given expression? Or a #command which will tell me coercions to a particular type?

view this post on Zulip Edward Ayers (Aug 11 2018 at 11:55):

I can't figure out how to use
set_option pp.coercions true

view this post on Zulip Simon Hudon (Aug 11 2018 at 16:10):

I only spotted this because I happen to be reading tactic.lean currently.

Good read! Don't spoil the ending though!

view this post on Zulip Simon Hudon (Aug 11 2018 at 16:10):

Does anyone know if there is a way to discover what coercions are occurring in a given expression?

#print instances has_coe

Last updated: May 13 2021 at 22:15 UTC