Stream: Coq users

Topic: Typeclasses and Print

view this post on Zulip Jerome Hugues (May 11 2023 at 14:29):


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?


view this post on Zulip Pierre Roux (May 11 2023 at 14:33):

Eval simpl in @rat _ OptionMonad _. (or Eval hnf or Eval compute) depending on what you want.

Last updated: Jun 20 2024 at 13:02 UTC