diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md
new file mode 100644
index 0000000000..70ba07b654
--- /dev/null
+++ b/plugins/hls-tactics-plugin/COMMANDS.md
@@ -0,0 +1,502 @@
+# Wingman Metaprogram Command Reference
+
+## application
+
+arguments: none.  
+non-deterministic.
+
+> Apply any function in the hypothesis that returns the correct type.
+
+
+### Example
+
+Given:
+
+```haskell
+f :: a -> b
+
+_ :: b
+```
+
+running  `application` will produce:
+
+```haskell
+f (_ :: a)
+```
+## apply
+
+arguments: single reference.  
+deterministic.
+
+> Apply the given function from *local* scope.
+
+
+### Example
+
+Given:
+
+```haskell
+f :: a -> b
+
+_ :: b
+```
+
+running  `apply f` will produce:
+
+```haskell
+f (_ :: a)
+```
+## assume
+
+arguments: single reference.  
+deterministic.
+
+> Use the given term from the hypothesis, unifying it with the current goal
+
+
+### Example
+
+Given:
+
+```haskell
+some_a_val :: a
+
+_ :: a
+```
+
+running  `assume some_a_val` will produce:
+
+```haskell
+some_a_val
+```
+## assumption
+
+arguments: none.  
+non-deterministic.
+
+> Use any term in the hypothesis that can unify with the current goal.
+
+
+### Example
+
+Given:
+
+```haskell
+some_a_val :: a
+
+_ :: a
+```
+
+running  `assumption` will produce:
+
+```haskell
+some_a_val
+```
+## auto
+
+arguments: none.  
+non-deterministic.
+
+> Repeatedly attempt to split, destruct, apply functions, and recurse in an attempt to fill the hole.
+
+
+### Example
+
+Given:
+
+```haskell
+f :: a -> b
+g :: b -> c
+
+_ :: a -> c
+```
+
+running  `auto` will produce:
+
+```haskell
+g . f
+```
+## binary
+
+arguments: none.  
+deterministic.
+
+> Produce a hole for a two-parameter function, as well as holes for its arguments. The argument holes have the same type but are otherwise unconstrained, and will be solved before the function.
+
+
+### Example
+
+> In the example below, the variable `a` is free, and will unify to the resulting extract from any subsequent tactic.
+
+Given:
+
+```haskell
+_ :: Int
+```
+
+running  `binary` will produce:
+
+```haskell
+(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)
+```
+## cata
+
+arguments: single reference.  
+deterministic.
+
+> Destruct the given term, recursing on every resulting binding.
+
+
+### Example
+
+> Assume we're called in the context of a function `f.`
+
+Given:
+
+```haskell
+x :: (a, a)
+
+_ 
+```
+
+running  `cata x` will produce:
+
+```haskell
+case x of
+  (a1, a2) ->
+    let a1_c = f a1
+        a2_c = f a2
+     in _
+```
+## collapse
+
+arguments: none.  
+deterministic.
+
+> Collapse every term in scope with the same type as the goal.
+
+
+### Example
+
+Given:
+
+```haskell
+a1 :: a
+a2 :: a
+a3 :: a
+
+_ :: a
+```
+
+running  `collapse` will produce:
+
+```haskell
+(_ :: a -> a -> a -> a) a1 a2 a3
+```
+## ctor
+
+arguments: single reference.  
+deterministic.
+
+> Use the given data cosntructor.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: Maybe a
+```
+
+running  `ctor Just` will produce:
+
+```haskell
+Just (_ :: a)
+```
+## destruct
+
+arguments: single reference.  
+deterministic.
+
+> Pattern match on the argument.
+
+
+### Example
+
+Given:
+
+```haskell
+a :: Bool
+
+_ 
+```
+
+running  `destruct a` will produce:
+
+```haskell
+case a of
+  False -> _
+  True -> _
+```
+## destruct_all
+
+arguments: none.  
+deterministic.
+
+> Pattern match on every function paramater, in original binding order.
+
+
+### Example
+
+> Assume `a` and `b` were bound via `f a b = _`.
+
+Given:
+
+```haskell
+a :: Bool
+b :: Maybe Int
+
+_ 
+```
+
+running  `destruct_all` will produce:
+
+```haskell
+case a of
+  False -> case b of
+    Nothing -> _
+    Just i -> _
+  True -> case b of
+    Nothing -> _
+    Just i -> _
+```
+## homo
+
+arguments: single reference.  
+deterministic.
+
+> Pattern match on the argument, and fill the resulting hole in with the same data constructor.
+
+
+### Example
+
+> Only applicable when the type constructor of the argument is the same as that of the hole.
+
+Given:
+
+```haskell
+e :: Either a b
+
+_ :: Either x y
+```
+
+running  `homo e` will produce:
+
+```haskell
+case e of
+  Left a -> Left (_ :: x)
+  Right b -> Right (_ :: y)
+```
+## intro
+
+arguments: single binding.  
+deterministic.
+
+> Construct a lambda expression, binding an argument with the given name.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: a -> b -> c -> d
+```
+
+running  `intro aye` will produce:
+
+```haskell
+\aye -> (_ :: b -> c -> d)
+```
+## intros
+
+arguments: varadic binding.  
+deterministic.
+
+> Construct a lambda expression, using the specific names if given, generating unique names otherwise. When no arguments are given, all of the function arguments will be bound; otherwise, this tactic will bind only enough to saturate the given names. Extra names are ignored.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: a -> b -> c -> d
+```
+
+running  `intros` will produce:
+
+```haskell
+\a b c -> (_ :: d)
+```
+
+### Example
+
+Given:
+
+```haskell
+_ :: a -> b -> c -> d
+```
+
+running  `intros aye` will produce:
+
+```haskell
+\aye -> (_ :: b -> c -> d)
+```
+
+### Example
+
+Given:
+
+```haskell
+_ :: a -> b -> c -> d
+```
+
+running  `intros x y z w` will produce:
+
+```haskell
+\x y z -> (_ :: d)
+```
+## obvious
+
+arguments: none.  
+non-deterministic.
+
+> Produce a nullary data constructor for the current goal.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: [a]
+```
+
+running  `obvious` will produce:
+
+```haskell
+[]
+```
+## recursion
+
+arguments: none.  
+deterministic.
+
+> Fill the current hole with a call to the defining function.
+
+
+### Example
+
+> In the context of `foo (a :: Int) (b :: b) = _`:
+
+Given:
+
+```haskell
+_ 
+```
+
+running  `recursion` will produce:
+
+```haskell
+foo (_ :: Int) (_ :: b)
+```
+## sorry
+
+arguments: none.  
+deterministic.
+
+> "Solve" the goal by leaving a hole.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: b
+```
+
+running  `sorry` will produce:
+
+```haskell
+_ :: b
+```
+## split
+
+arguments: none.  
+non-deterministic.
+
+> Produce a data constructor for the current goal.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: Either a b
+```
+
+running  `split` will produce:
+
+```haskell
+Right (_ :: b)
+```
+## unary
+
+arguments: none.  
+deterministic.
+
+> Produce a hole for a single-parameter function, as well as a hole for its argument. The argument holes are completely unconstrained, and will be solved before the function.
+
+
+### Example
+
+> In the example below, the variable `a` is free, and will unify to the resulting extract from any subsequent tactic.
+
+Given:
+
+```haskell
+_ :: Int
+```
+
+running  `unary` will produce:
+
+```haskell
+(_2 :: a -> Int) (_1 :: a)
+```
+## use
+
+arguments: single reference.  
+deterministic.
+
+> Apply the given function from *module* scope.
+
+
+### Example
+
+> `import Data.Char (isSpace)`
+
+Given:
+
+```haskell
+_ :: Bool
+```
+
+running  `use isSpace` will produce:
+
+```haskell
+isSpace (_ :: Char)
+```
diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index 3a18e9393e..ee9bb2be28 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -47,6 +47,7 @@ library
     Wingman.Machinery
     Wingman.Metaprogramming.Lexer
     Wingman.Metaprogramming.Parser
+    Wingman.Metaprogramming.Parser.Documentation
     Wingman.Metaprogramming.ProofState
     Wingman.Naming
     Wingman.Plugin
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index b988d08dac..a2f503109d 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -19,6 +19,7 @@ import           Wingman.Auto
 import           Wingman.Context (getCurrentDefinitions)
 import           Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext)
 import           Wingman.Metaprogramming.Lexer
+import           Wingman.Metaprogramming.Parser.Documentation
 import           Wingman.Metaprogramming.ProofState (proofState, layout)
 import           Wingman.Tactics
 import           Wingman.Types
@@ -42,44 +43,316 @@ variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
 variadic_occ name tac = tac <$> (identifier name *> P.many variable)
 
 
+commands :: [SomeMetaprogramCommand]
+commands =
+  [ command "assumption" Nondeterministic Nullary
+      "Use any term in the hypothesis that can unify with the current goal."
+      (pure assumption)
+      [ Example
+          Nothing
+          []
+          [EHI "some_a_val" "a"]
+          (Just "a")
+          "some_a_val"
+      ]
+
+  , command "assume" Deterministic (Ref One)
+      "Use the given term from the hypothesis, unifying it with the current goal"
+      (pure . assume)
+      [ Example
+          Nothing
+          ["some_a_val"]
+          [EHI "some_a_val" "a"]
+          (Just "a")
+          "some_a_val"
+      ]
+
+  , command "intros" Deterministic (Bind Many)
+      ( mconcat
+          [ "Construct a lambda expression, using the specific names if given, "
+          , "generating unique names otherwise. When no arguments are given, "
+          , "all of the function arguments will be bound; otherwise, this "
+          , "tactic will bind only enough to saturate the given names. Extra "
+          , "names are ignored."
+          ])
+      (pure . \case
+        []    -> intros
+        names -> intros' $ Just names
+      )
+      [ Example
+          Nothing
+          []
+          []
+          (Just "a -> b -> c -> d")
+          "\\a b c -> (_ :: d)"
+      , Example
+          Nothing
+          ["aye"]
+          []
+          (Just "a -> b -> c -> d")
+          "\\aye -> (_ :: b -> c -> d)"
+      , Example
+          Nothing
+          ["x", "y", "z", "w"]
+          []
+          (Just "a -> b -> c -> d")
+          "\\x y z -> (_ :: d)"
+      ]
+
+  , command "intro" Deterministic (Bind One)
+      "Construct a lambda expression, binding an argument with the given name."
+      (pure . intros' . Just . pure)
+      [ Example
+          Nothing
+          ["aye"]
+          []
+          (Just "a -> b -> c -> d")
+          "\\aye -> (_ :: b -> c -> d)"
+      ]
+
+  , command "destruct_all" Deterministic Nullary
+      "Pattern match on every function paramater, in original binding order."
+      (pure destructAll)
+      [ Example
+          (Just "Assume `a` and `b` were bound via `f a b = _`.")
+          []
+          [EHI "a" "Bool", EHI "b" "Maybe Int"]
+          Nothing $
+          T.pack $ init $ unlines
+            [ "case a of"
+            , "  False -> case b of"
+            , "    Nothing -> _"
+            , "    Just i -> _"
+            , "  True -> case b of"
+            , "    Nothing -> _"
+            , "    Just i -> _"
+            ]
+      ]
+
+  , command "destruct" Deterministic (Ref One)
+      "Pattern match on the argument."
+      (pure . useNameFromHypothesis destruct)
+      [ Example
+          Nothing
+          ["a"]
+          [EHI "a" "Bool"]
+          Nothing $
+          T.pack $ init $ unlines
+            [ "case a of"
+            , "  False -> _"
+            , "  True -> _"
+            ]
+      ]
+
+  , command "homo" Deterministic (Ref One)
+      ( mconcat
+        [ "Pattern match on the argument, and fill the resulting hole in with "
+        , "the same data constructor."
+        ])
+      (pure . useNameFromHypothesis homo)
+      [ Example
+          (Just $ mconcat
+            [ "Only applicable when the type constructor of the argument is "
+            , "the same as that of the hole."
+            ])
+          ["e"]
+          [EHI "e" "Either a b"]
+          (Just "Either x y") $
+          T.pack $ init $ unlines
+            [ "case e of"
+            , "  Left a -> Left (_ :: x)"
+            , "  Right b -> Right (_ :: y)"
+            ]
+      ]
+
+  , command "application" Nondeterministic Nullary
+      "Apply any function in the hypothesis that returns the correct type."
+      (pure application)
+      [ Example
+          Nothing
+          []
+          [EHI "f" "a -> b"]
+          (Just "b")
+          "f (_ :: a)"
+      ]
+
+  , command "apply" Deterministic (Ref One)
+      "Apply the given function from *local* scope."
+      (pure . useNameFromHypothesis apply)
+      [ Example
+          Nothing
+          ["f"]
+          [EHI "f" "a -> b"]
+          (Just "b")
+          "f (_ :: a)"
+      ]
+
+  , command "split" Nondeterministic Nullary
+      "Produce a data constructor for the current goal."
+      (pure split)
+      [ Example
+          Nothing
+          []
+          []
+          (Just "Either a b")
+          "Right (_ :: b)"
+      ]
+
+  , command "ctor" Deterministic (Ref One)
+      "Use the given data cosntructor."
+      (pure . userSplit)
+      [ Example
+          Nothing
+          ["Just"]
+          []
+          (Just "Maybe a")
+          "Just (_ :: a)"
+      ]
+
+  , command "obvious" Nondeterministic Nullary
+      "Produce a nullary data constructor for the current goal."
+      (pure obvious)
+      [ Example
+          Nothing
+          []
+          []
+          (Just "[a]")
+          "[]"
+      ]
+
+  , command "auto" Nondeterministic Nullary
+      ( mconcat
+          [ "Repeatedly attempt to split, destruct, apply functions, and "
+          , "recurse in an attempt to fill the hole."
+          ])
+      (pure auto)
+      [ Example
+          Nothing
+          []
+          [EHI "f" "a -> b", EHI "g" "b -> c"]
+          (Just "a -> c")
+          "g . f"
+      ]
+
+  , command "sorry" Deterministic Nullary
+      "\"Solve\" the goal by leaving a hole."
+      (pure sorry)
+      [ Example
+          Nothing
+          []
+          []
+          (Just "b")
+          "_ :: b"
+      ]
+
+  , command "unary" Deterministic Nullary
+      ( mconcat
+        [ "Produce a hole for a single-parameter function, as well as a hole for "
+        , "its argument. The argument holes are completely unconstrained, and "
+        , "will be solved before the function."
+        ])
+      (pure $ nary 1)
+      [ Example
+          (Just $ mconcat
+            [ "In the example below, the variable `a` is free, and will unify "
+            , "to the resulting extract from any subsequent tactic."
+            ])
+          []
+          []
+          (Just "Int")
+          "(_2 :: a -> Int) (_1 :: a)"
+      ]
+
+  , command "binary" Deterministic Nullary
+      ( mconcat
+        [ "Produce a hole for a two-parameter function, as well as holes for "
+        , "its arguments. The argument holes have the same type but are "
+        , "otherwise unconstrained, and will be solved before the function."
+        ])
+      (pure $ nary 2)
+      [ Example
+          (Just $ mconcat
+            [ "In the example below, the variable `a` is free, and will unify "
+            , "to the resulting extract from any subsequent tactic."
+            ])
+          []
+          []
+          (Just "Int")
+          "(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)"
+      ]
+
+  , command "recursion" Deterministic Nullary
+      "Fill the current hole with a call to the defining function."
+      ( pure $
+          fmap listToMaybe getCurrentDefinitions >>= \case
+            Just (self, _) -> useNameFromContext apply self
+            Nothing -> E.throwError $ TacticPanic "no defining function"
+      )
+      [ Example
+          (Just "In the context of `foo (a :: Int) (b :: b) = _`:")
+          []
+          []
+          Nothing
+          "foo (_ :: Int) (_ :: b)"
+      ]
+
+  , command "use" Deterministic (Ref One)
+      "Apply the given function from *module* scope."
+      ( \occ -> do
+          ctx <- asks ps_context
+          ty <- case lookupNameInContext occ ctx of
+            Just ty -> pure ty
+            Nothing -> CType <$> getOccTy occ
+          pure $ apply $ createImportedHyInfo occ ty
+      )
+      [ Example
+          (Just "`import Data.Char (isSpace)`")
+          ["isSpace"]
+          []
+          (Just "Bool")
+          "isSpace (_ :: Char)"
+      ]
+
+  , command "cata" Deterministic (Ref One)
+      "Destruct the given term, recursing on every resulting binding."
+      (pure . useNameFromHypothesis cata)
+      [ Example
+          (Just "Assume we're called in the context of a function `f.`")
+          ["x"]
+          [EHI "x" "(a, a)"]
+          Nothing $
+          T.pack $ init $ unlines
+            [ "case x of"
+            , "  (a1, a2) ->"
+            , "    let a1_c = f a1"
+            , "        a2_c = f a2"
+            , "     in _"
+            ]
+      ]
+
+  , command "collapse" Deterministic Nullary
+      "Collapse every term in scope with the same type as the goal."
+      (pure collapse)
+      [ Example
+          Nothing
+          []
+          [ EHI "a1" "a"
+          , EHI "a2" "a"
+          , EHI "a3" "a"
+          ]
+          (Just "a")
+          "(_ :: a -> a -> a -> a) a1 a2 a3"
+      ]
+
+  ]
+
+
+
 oneTactic :: Parser (TacticsM ())
 oneTactic =
   P.choice
-    [ braces tactic
-      -- TODO(sandy): lean uses braces for control flow, but i always forget
-      -- and want to use parens. is there a semantic difference?
-    , parens tactic
-    , nullary   "assumption" assumption
-    , unary_occ "assume" assume
-    , variadic_occ   "intros" $ \case
-        []    -> intros
-        names -> intros' $ Just names
-    , unary_occ  "intro" $ intros' . Just . pure
-    , nullary   "destruct_all" destructAll
-    , unary_occ "destruct" $ useNameFromHypothesis destruct
-    , unary_occ "homo" $ useNameFromHypothesis homo
-    , nullary   "application" application
-    , unary_occ "apply_module" $ useNameFromContext apply
-    , unary_occ "apply" $ useNameFromHypothesis apply
-    , nullary   "split" split
-    , unary_occ "ctor" userSplit
-    , nullary   "obvious" obvious
-    , nullary   "auto" auto
-    , nullary   "sorry" sorry
-    , nullary   "unary" $ nary 1
-    , nullary   "binary" $ nary 2
-    , unary_occ "cata" $ useNameFromHypothesis cata
-    , nullary   "collapse" collapse
-    , nullary   "recursion" $
-        fmap listToMaybe getCurrentDefinitions >>= \case
-          Just (self, _) -> useNameFromContext apply self
-          Nothing -> E.throwError $ TacticPanic "no defining function"
-    , unary_occM "use" $ \occ -> do
-        ctx <- asks ps_context
-        ty <- case lookupNameInContext occ ctx of
-          Just ty -> pure ty
-          Nothing -> CType <$> getOccTy occ
-        pure $ apply $ createImportedHyInfo occ ty
+    [ parens tactic
+    , makeParser commands
     ]
 
 
@@ -147,3 +420,15 @@ getOccTy occ = do
   mty <- liftIO $ getOccNameType hscenv rdrenv modul occ
   maybe (fail $ occNameString occ <> " is not in scope") pure mty
 
+
+------------------------------------------------------------------------------
+-- | Automatically generate the metaprogram command reference.
+writeDocumentation :: IO ()
+writeDocumentation =
+  writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $
+    unlines
+      [ "# Wingman Metaprogram Command Reference"
+      , ""
+      , prettyReadme commands
+      ]
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs
new file mode 100644
index 0000000000..9347c944ab
--- /dev/null
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs
@@ -0,0 +1,228 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Wingman.Metaprogramming.Parser.Documentation where
+
+import           Data.Functor ((<&>))
+import           Data.List (sortOn)
+import           Data.String (IsString)
+import           Data.Text (Text)
+import           Data.Text.Prettyprint.Doc
+import           Data.Text.Prettyprint.Doc.Render.String (renderString)
+import           GhcPlugins (OccName)
+import qualified Text.Megaparsec as P
+import           Wingman.Metaprogramming.Lexer (Parser, identifier, variable)
+import           Wingman.Types (TacticsM)
+
+
+------------------------------------------------------------------------------
+-- | Is a tactic deterministic or not?
+data Determinism
+  = Deterministic
+  | Nondeterministic
+
+prettyDeterminism :: Determinism -> Doc b
+prettyDeterminism Deterministic = "deterministic"
+prettyDeterminism Nondeterministic = "non-deterministic"
+
+
+------------------------------------------------------------------------------
+-- | How many arguments does the tactic take?
+data Count a where
+  One  :: Count OccName
+  Many :: Count [OccName]
+
+prettyCount :: Count a -> Doc b
+prettyCount One  = "single"
+prettyCount Many = "varadic"
+
+
+------------------------------------------------------------------------------
+-- | What sorts of arguments does the tactic take? Currently there is no
+-- distincion between 'Ref' and 'Bind', other than documentation.
+--
+-- The type index here is used for the shape of the function the parser should
+-- take.
+data Syntax a where
+  Nullary :: Syntax (Parser (TacticsM ()))
+  Ref     :: Count a -> Syntax (a -> Parser (TacticsM ()))
+  Bind    :: Count a -> Syntax (a -> Parser (TacticsM ()))
+
+prettySyntax :: Syntax a -> Doc b
+prettySyntax Nullary   = "none"
+prettySyntax (Ref co)  = prettyCount co <+> "reference"
+prettySyntax (Bind co) = prettyCount co <+> "binding"
+
+
+------------------------------------------------------------------------------
+-- | An example for the documentation.
+data Example = Example
+  { ex_ctx    :: Maybe Text         -- ^ Specific context information about when the tactic is applicable
+  , ex_args   :: [Var]              -- ^ Arguments the tactic was called with
+  , ex_hyp    :: [ExampleHyInfo]    -- ^ The hypothesis
+  , ex_goal   :: Maybe ExampleType  -- ^ Current goal. Nothing indicates it's uninteresting.
+  , ex_result :: Text               -- ^ Resulting extract.
+  }
+
+
+------------------------------------------------------------------------------
+-- | An example 'HyInfo'.
+data ExampleHyInfo = EHI
+  { ehi_name :: Var          -- ^ Name of the variable
+  , ehi_type :: ExampleType  -- ^ Type of the variable
+  }
+
+
+------------------------------------------------------------------------------
+-- | A variable
+newtype Var = Var
+  { getVar :: Text
+  }
+  deriving newtype (IsString, Pretty)
+
+
+------------------------------------------------------------------------------
+-- | A type
+newtype ExampleType = ExampleType
+  { getExampleType :: Text
+  }
+  deriving newtype (IsString, Pretty)
+
+
+------------------------------------------------------------------------------
+-- | A command to expose to the parser
+data MetaprogramCommand a = MC
+  { mpc_name        :: Text         -- ^ Name of the command. This is the token necessary to run the command.
+  , mpc_syntax      :: Syntax a     -- ^ The command's arguments
+  , mpc_det         :: Determinism  -- ^ Determinism of the command
+  , mpc_description :: Text         -- ^ User-facing description
+  , mpc_tactic      :: a            -- ^ Tactic to run
+  , mpc_examples    :: [Example]    -- ^ Collection of documentation examples
+  }
+
+------------------------------------------------------------------------------
+-- | Existentialize the pain away
+data SomeMetaprogramCommand where
+  SMC :: MetaprogramCommand a -> SomeMetaprogramCommand
+
+
+------------------------------------------------------------------------------
+-- | Run the 'Parser' of a 'MetaprogramCommand'
+makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())
+makeMPParser (MC name Nullary _ _ tactic _) = do
+  identifier name
+  tactic
+makeMPParser (MC name (Ref One) _ _ tactic _) = do
+  identifier name
+  variable >>= tactic
+makeMPParser (MC name (Ref Many) _ _ tactic _) = do
+  identifier name
+  P.many variable >>= tactic
+makeMPParser (MC name (Bind One) _ _ tactic _) = do
+  identifier name
+  variable >>= tactic
+makeMPParser (MC name (Bind Many) _ _ tactic _) = do
+  identifier name
+  P.many variable >>= tactic
+
+
+------------------------------------------------------------------------------
+-- | Compile a collection of metaprogram commands into a parser.
+makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ())
+makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp
+
+
+------------------------------------------------------------------------------
+-- | Pretty print a command.
+prettyCommand :: MetaprogramCommand a -> Doc b
+prettyCommand (MC name syn det desc _ exs) = vsep
+  [ "##" <+> pretty name
+  , mempty
+  , "arguments:" <+> prettySyntax syn <> ".  "
+  , prettyDeterminism det <> "."
+  , mempty
+  , ">" <+> align (pretty desc)
+  , mempty
+  , vsep $ fmap (prettyExample name) exs
+  ]
+
+
+------------------------------------------------------------------------------
+-- | Pretty print a hypothesis.
+prettyHyInfo :: ExampleHyInfo -> Doc a
+prettyHyInfo hi = pretty (ehi_name hi) <+> "::" <+> pretty (ehi_type hi)
+
+
+------------------------------------------------------------------------------
+-- | Append the given term only if the first argument has elements.
+mappendIfNotNull :: [a] -> a -> [a]
+mappendIfNotNull [] _ = []
+mappendIfNotNull as a = as <> [a]
+
+
+------------------------------------------------------------------------------
+-- | Pretty print an example.
+prettyExample :: Text -> Example -> Doc a
+prettyExample name (Example m_txt args hys goal res) =
+  align $ vsep
+    [ mempty
+    , "### Example"
+    , maybe mempty ((line <>) . (<> line) . (">" <+>) . align . pretty) m_txt
+    , "Given:"
+    , mempty
+    , codeFence $ vsep
+        $ mappendIfNotNull (fmap prettyHyInfo hys) mempty
+           <> [ "_" <+> maybe mempty (("::" <+>). pretty) goal
+              ]
+    , mempty
+    , hsep
+        [ "running "
+        , enclose "`" "`" $ pretty name <> hsep (mempty : fmap pretty args)
+        , "will produce:"
+        ]
+    , mempty
+    , codeFence $ align $ pretty res
+    ]
+
+
+------------------------------------------------------------------------------
+-- | Make a haskell code fence.
+codeFence :: Doc a -> Doc a
+codeFence d = align $ vsep
+  [ "```haskell"
+  , d
+  , "```"
+  ]
+
+
+------------------------------------------------------------------------------
+-- | Render all of the commands.
+prettyReadme :: [SomeMetaprogramCommand] -> String
+prettyReadme
+  = renderString
+  . layoutPretty defaultLayoutOptions
+  . vsep
+  . fmap (\case SMC c -> prettyCommand c)
+  . sortOn (\case SMC c -> mpc_name c)
+
+
+
+------------------------------------------------------------------------------
+-- | Helper function to build a 'SomeMetaprogramCommand'.
+command
+    :: Text
+    -> Determinism
+    -> Syntax a
+    -> Text
+    -> a
+    -> [Example]
+    -> SomeMetaprogramCommand
+command txt det syn txt' a exs = SMC $
+  MC
+    { mpc_name        = txt
+    , mpc_det         = det
+    , mpc_syntax      = syn
+    , mpc_description = txt'
+    , mpc_tactic      = a
+    , mpc_examples    = exs
+    }
+