Hi,
I am experimenting with monads and typeclasses recently to better understand the fundamentals.
I could do the following
Example step4 := @ret _ OptionMonad _ 7.
Compute step4.
Check @ret _ OptionMonad _ .
and get the results I expect: a value being computed and the type of the function.
I would like to inspect the actual implementation of ret used in the previous calls. That is in the context of the calls above. My use case is purely for illustrating/debugging. I am looking for something along the line of
Print @ret _ OptionMonad _.
but this is rejected, and from the documentation it seems it is for very valid reasons.
Is there a way to emulate this behavior using some other approaches?
Thanks
Eval simpl in @rat _ OptionMonad _.
(or Eval hnf
or Eval compute
) depending on what you want.
Last updated: Oct 13 2024 at 01:02 UTC