accessing MetaM from IO

Stream: lean4

[Arthur Paulino]

Suppose I have a function A whose return type is IO String and another function B whose return type is MetaM String.
Is there a way to call let x : String ← B <args> inside A?
Detail: I have an instance of Environment as an input of A that can be used, if needed.
C.C.: @Tomas Skrivan

[Tomas Skrivan]

I would phrase the question a bit differently. Given e : Environment can you initialize fresh state of MetaM and execute some functions in MetaM like whnf and then obtain the value i.e. turn for example MetaM String to Option String (none if some exception happened)?

[Arthur Paulino]

That's indeed a better way to put it

[Mac]

@Arthur Paulino both MetaM and CoreM have a lot of settings that you may wish to configure, but here is the most minimal example:

#eval show IO _ from do
  let env : Environment := arbitrary
  let act : MetaM PUnit := pure ()
  Prod.fst <$> act.run'.toIO {} {env}