## Stream: general

#### Koundinya Vajjha (Feb 21 2019 at 22:34):

I have a termns : list name, and a function foo : name -> tactic string. What I want is a term of type list (list string). Naturally, I want to use some sort of map to apply foo to every element of ns, but that gives me the wrong type. What do I do to get rid of the tactic monad?

#### Kevin Buzzard (Feb 21 2019 at 23:01):

Isn't it in general impossible to get out of a monad?

#### Kevin Buzzard (Feb 21 2019 at 23:02):

The tactic could fail; then there's no possibility for getting out

#### Chris Hughes (Feb 21 2019 at 23:21):

list.mmap might help. You'll end up with a tactic (list (list string))

#### Koundinya Vajjha (Feb 21 2019 at 23:23):

Yes I guess so. I figured it out - at any rate. Thanks!