run_cmd, monads, and tests for their methods

Stream: new members

[Eduardo Ochs]

Hi all,

I'm finally starting to understand this comment about how run_cmd works...

The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
except that it doesn't print an empty diagnostic.

[Eduardo Ochs]

This snippet has lots of interesting tests and pointers:

import Lean
import Lean.Elab.Command
open   Lean.Elab.Command
open   Lean

namespace Foo
run_cmd                                  logInfo (← getCurrNamespace)
#eval  show  CommandElabM Unit  from  do logInfo (← getCurrNamespace)
#eval  show (CommandElabM Unit) from (do logInfo (← getCurrNamespace))
#check show (CommandElabM Unit) from (do logInfo (← getCurrNamespace))
#check                                do logInfo (← getCurrNamespace)
#check                                   logInfo
#check                                              getCurrNamespace
#check      CommandElabM Unit
#check      CommandElabM

#check AddMessageContext
#check MessageData
#check MonadLog
#check MonadOptions
#check logInfo

[Eduardo Ochs]

The code inside the logInfo has access to lots of monads, and (← getCurrNamespace) is just a simple example of what we can do there.

[Eduardo Ochs]

Question: is there a place in which I can find tests for the methods of those classes? For example, I would like to learn how to use the method getOpenDecls, from:

class MonadResolveName (m : Type → Type) where
  getCurrNamespace   : m Name
  getOpenDecls       : m (List OpenDecl)

right now the only way that I have to learn something like that is by spending many hours reading the sources, to try to create arguments with the right types to test these methods... is there a better way, like a place with tests that can be used as examples?