## Stream: general

### Topic: Potential vm bug

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

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


#### Edward Ayers (Aug 11 2018 at 11:33):

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

Ah, cheers!

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

#### Edward Ayers (Aug 11 2018 at 11:55):

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

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

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