diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md
index be3cc59b399e0f13abb2f5bec5037ed0ffca0b3f..6a1c00b561db8f5764cd0f520db748760a7e01b3 100644
--- a/plugins/hls-tactics-plugin/COMMANDS.md
+++ b/plugins/hls-tactics-plugin/COMMANDS.md
@@ -382,6 +382,32 @@ running  `intros x y z w` will produce:
 \x y z -> (_ :: d)
 ```
 
+## let
+
+arguments: varadic binding.  
+deterministic.
+
+> Create let-bindings for each binder given to this tactic.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: x
+```
+
+running  `let a b c` will produce:
+
+```haskell
+let a = _1 :: a
+    b = _2 :: b
+    c = _3 :: c
+ in (_4 :: x)
+
+```
+
 ## nested
 
 arguments: single reference.  
diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 57afba70e9e2a488c152fe2ec3f5f74c0a77f134..07b112e01ac27baad87d79f2c86fad5465cc6f10 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -15,6 +15,7 @@ import           Control.Lens ((%~), (<>~), (&))
 import           Control.Monad.Except
 import           Control.Monad.Reader (ask)
 import           Control.Monad.State
+import           Data.Bifunctor (second)
 import           Data.Bool (bool)
 import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
@@ -315,3 +316,23 @@ letForEach rename solve (unHypothesis -> hy) jdg = do
       g <- fmap (fmap unLoc) $ newSubgoal $ introduce ctx (userHypothesis hy') jdg
       pure $ fmap noLoc $ let' <$> matches <*> g
 
+
+------------------------------------------------------------------------------
+-- | Let-bind the given occname judgement pairs.
+nonrecLet
+    :: [(OccName, Judgement)]
+    -> Judgement
+    -> RuleM (Synthesized (LHsExpr GhcPs))
+nonrecLet occjdgs jdg = do
+  occexts <- traverse newSubgoal $ fmap snd occjdgs
+  ctx     <- ask
+  ext     <- newSubgoal
+           $ introduce ctx (userHypothesis $ fmap (second jGoal) occjdgs)
+           $ jdg
+  pure $ fmap noLoc $
+    let'
+      <$> traverse
+            (\(occ, ext) -> valBind (occNameToStr occ) <$> fmap unLoc ext)
+            (zip (fmap fst occjdgs) occexts)
+      <*> fmap unLoc ext
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index d22c20363e26744c9853e2a73d565f15807d8d7c..c16b9dca70201e2b5764626ebc56da175e55a50a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
@@ -348,6 +348,22 @@ commands =
           "(_ :: a -> a -> a -> a) a1 a2 a3"
       ]
 
+  , command "let" Deterministic (Bind Many)
+      "Create let-bindings for each binder given to this tactic."
+      (pure . letBind)
+      [ Example
+          Nothing
+          ["a", "b", "c"]
+          [ ]
+          (Just "x")
+          $ T.pack $ unlines
+            [ "let a = _1 :: a"
+            , "    b = _2 :: b"
+            , "    c = _3 :: c"
+            , " in (_4 :: x)"
+            ]
+      ]
+
   , command "try" Nondeterministic Tactic
       "Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states."
       (pure . R.try)
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index a853335e35ce4581e23a88675c5350b21aaae2d5..9075acb3b089f3eed4e1c345ff40e440b837d9a9 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
 
 module Wingman.Tactics
   ( module Wingman.Tactics
@@ -23,6 +24,7 @@ import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Set (Set)
 import qualified Data.Set as S
+import           Data.Traversable (for)
 import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts
@@ -579,6 +581,19 @@ cata hi = do
       $ Hypothesis unifiable_diff
 
 
+letBind :: [OccName] -> TacticsM ()
+letBind occs = do
+  jdg <- goal
+  occ_tys <- for occs
+           $ \occ
+          -> fmap (occ, )
+           $ fmap (<$ jdg)
+           $ fmap CType
+           $ freshTyvars
+           $ mkInvForAllTys [alphaTyVar] alphaTy
+  rule $ nonrecLet occ_tys
+
+
 ------------------------------------------------------------------------------
 -- | Deeply nest an unsaturated function onto itself
 nested :: OccName -> TacticsM ()
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
index 94eb664ab955a88b88dd2ff73c8e2f34929d8fe7..2fdf6a89365c1dad36db26bdb09a317711b82e9b 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
@@ -39,5 +39,7 @@ spec = do
     metaTest  4 28 "MetaUseSymbol"
     metaTest  7 53 "MetaDeepOf"
     metaTest  2 34 "MetaWithArg"
+    metaTest  2 18 "MetaLetSimple"
+
     metaTest  2 12 "IntrosTooMany"
 
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.expected.hs
new file mode 100644
index 0000000000000000000000000000000000000000..54c3678c21f6b251adb79b4e2bdb2b1359068566
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.expected.hs
@@ -0,0 +1,7 @@
+test :: Int
+test
+  = let
+      a = _w0
+      b = _w1
+      c = _w2
+    in _w3
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.hs b/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ae570bae7bf3e937500784d22b06f1f213ee9659
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.hs
@@ -0,0 +1,2 @@
+test :: Int
+test = [wingman| let a b c |]