diff --git a/Tactics/QuoteLight.lean b/Tactics/QuoteLight.lean
new file mode 100644
index 00000000..29966254
--- /dev/null
+++ b/Tactics/QuoteLight.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Lean
+import Tactics.QuoteLight.ToExpr
+
+open Lean Meta Elab.Term
+
+namespace QuoteLight
+
+/-- `QL α` is a Lean `Expr` of type `α`, see the `ql(..)` and `QL(..)` macros
+for
+
+It's primary utility is to serve as machine-checked documentation of the
+expected type of expressions. However, the index is *not* actually checked,
+so it is entirely possible to construt  -/
+@[pp_using_anonymous_constructor]
+structure QL (α : Expr) where
+  ofExpr :: toExpr : Expr
+deriving Inhabited
+
+attribute [coe] QL.toExpr
+instance : CoeOut (QL α) Expr := ⟨QL.toExpr⟩
+
+/-- Given a closed term `t` of type `α` (i.e., `t` may not have free or meta variables) ,
+`ql(<t>)` will construct a Lean expression that represents `t`.
+You can think of it as a more powerful version of `ToExpr.toExpr`.
+
+For example, `ql(Nat)` will return the expression `.const ``Nat []`, and
+`ql(BitVec 64)` gives the same expression as
+  `.app (.const ``BitVec []) (toExpr 64)`
+-/
+elab "ql(" t:term ")" : term <= expectedType? => do
+  let t ← elabTerm t none
+  synthesizeSyntheticMVarsNoPostponing
+  let t ← instantiateMVars t
+
+  if t.hasFVar then
+    throwError "error: expression has free variables:\n  {t}\n\n\
+      ql only supports constant expressions"
+  else if t.hasMVar then
+    throwError "error: expression has meta variables:\n  {t}\n\n\
+      ql only supports constant expressions"
+
+  let expr := toExpr t
+  if expectedType? == Expr.const ``Expr [] then
+    /- If the exected type is `Expr`, then we output just the raw expression,
+       circumventing the need to apply the `QL` to `Expr` coercion.
+       This makes the result slightly cleaner. -/
+    return expr
+  else
+    let ty ← inferType t
+    let exprTy := toExpr ty
+    return mkApp2 (mkConst ``QL.ofExpr) exprTy expr
+
+/-- `QL(<t>)` returns `QL ql(<t>)`.
+
+For example, `QL(BitVec 64)` is the type of Lean expressions of type `BitVec 64`.
+-/
+macro "QL(" t:term ")" : term => `(QL ql($t))
+
+-- TODO: write a delaborator that delaborates applications of `QL` into
+--       the `QL(...)` macro for better readability
+
+/-!
+## Simple Tests
+-/
+section Test
+
+-- Basic check to ensure synthetic mvars get synthesized properly
+/--
+info: ⟨(Expr.const `List [Level.zero]).app
+    ((Expr.const `BitVec []).app
+      ((((Expr.const `OfNat.ofNat [Level.zero]).app (Expr.const `Nat [])).app (Expr.lit (Literal.natVal 64))).app
+        ((Expr.const `instOfNatNat []).app (Expr.lit (Literal.natVal 64)))))⟩ : QL (Expr.sort Level.zero.succ)
+-/
+#guard_msgs in #check ql(List (BitVec 64))
+
+-- Basic test for `QL(..)` macro
+/--
+info: QL
+  ((Expr.const `List [Level.zero]).app
+    ((Expr.const `BitVec []).app
+      ((((Expr.const `OfNat.ofNat [Level.zero]).app (Expr.const `Nat [])).app (Expr.lit (Literal.natVal 64))).app
+        ((Expr.const `instOfNatNat []).app (Expr.lit (Literal.natVal 64)))))) : Type
+-/
+#guard_msgs in #check QL(List (BitVec 64))
+
+-- Test that bound variables are handled properly
+/--
+info: ⟨Expr.lam `n (Expr.const `Nat []) ((Expr.const `BitVec []).app (Expr.bvar 0))
+    BinderInfo.default⟩ : QL (Expr.forallE `n (Expr.const `Nat []) (Expr.sort Level.zero.succ) BinderInfo.default)
+-/
+#guard_msgs in #check ql(fun n => BitVec n)
+
+-- Test that free variables are rejected
+/--
+error: error: expression has free variables:
+  BitVec n
+
+ql only supports constant expressions
+-/
+#guard_msgs in variable (n : Nat) in #check ql(BitVec n)
+
+end Test
+
+end QuoteLight
diff --git a/Tactics/QuoteLight/DeriveToExpr.lean b/Tactics/QuoteLight/DeriveToExpr.lean
new file mode 100644
index 00000000..32743285
--- /dev/null
+++ b/Tactics/QuoteLight/DeriveToExpr.lean
@@ -0,0 +1,230 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+Source: https://github.com/leanprover-community/mathlib4/blob/8d6f380fde8631e39a62b5a009b2ffec2eb3c17f/Mathlib/Tactic/DeriveToExpr.lean
+-/
+import Tactics.QuoteLight.ToLevel
+
+/-!
+# A `ToExpr` derive handler
+
+This module defines a `ToExpr` derive handler for inductive types. It supports mutually inductive
+types as well.
+
+The `ToExpr` derive handlers support universe level polymorphism. This is implemented using the
+`Lean.ToLevel` class. To use `ToExpr` in places where there is universe polymorphism, make sure
+to have a `[ToLevel.{u}]` instance available.
+
+**Warning:** Import `Mathlib.Tactic.ToExpr` instead of this one. This ensures that you are using
+the universe polymorphic `ToExpr` instances that override the ones from Lean 4 core.
+
+Implementation note: this derive handler was originally modeled after the `Repr` derive handler.
+-/
+
+namespace QuoteLight.Deriving.ToExpr
+
+open Lean Elab Lean.Parser.Term
+open Meta Command Deriving
+
+/-- Specialization of `Lean.Elab.Deriving.mkHeader` for `ToExpr`. -/
+def mkToExprHeader (indVal : InductiveVal) : TermElabM Header := do
+  -- The auxiliary functions we produce are `indtype -> Expr`.
+  let header ← mkHeader ``ToExpr 1 indVal
+  return header
+
+/-- Give a term that is equivalent to `(term| mkAppN $f #[$args,*])`.
+As an optimization, `mkAppN` is pre-expanded out to use `Expr.app` directly. -/
+def mkAppNTerm (f : Term) (args : Array Term) : MetaM Term :=
+  args.foldlM (fun a b => `(Expr.app $a $b)) f
+
+/-- Create the body of the `toExpr` function
+for the `ToExpr` instance, which is a `match` expression
+that calls `toExpr` and `toTypeExpr` to assemble an expression for a given term.
+For recursive inductive types, `auxFunName` refers to the `ToExpr` instance
+for the current type.
+For mutually recursive types, we rely on the local instances set up by `mkLocalInstanceLetDecls`. -/
+def mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) :
+    TermElabM Term := do
+  let discrs ← mkDiscrs header indVal
+  let alts ← mkAlts
+  `(match $[$discrs],* with $alts:matchAlt*)
+where
+  /-- Create the `match` cases, one per constructor. -/
+  mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do
+    let mut alts := #[]
+    for ctorName in indVal.ctors do
+      let ctorInfo ← getConstInfoCtor ctorName
+      let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do
+        let mut patterns := #[]
+        -- add `_` pattern for indices
+        for _ in [:indVal.numIndices] do
+          patterns := patterns.push (← `(_))
+        let mut ctorArgs := #[]
+        let mut rhsArgs : Array Term := #[]
+        let mkArg (x : Expr) (a : Term) : TermElabM Term := do
+          if (← inferType x).isAppOf indVal.name then
+            `($(mkIdent auxFunName) $a)
+          else if ← Meta.isType x then
+            `(toTypeExpr $a)
+          else
+            `(toExpr $a)
+        -- add `_` pattern for inductive parameters, which are inaccessible
+        for i in [:ctorInfo.numParams] do
+          let a := mkIdent header.argNames[i]!
+          ctorArgs := ctorArgs.push (← `(_))
+          rhsArgs := rhsArgs.push <| ← mkArg xs[i]! a
+        for i in [:ctorInfo.numFields] do
+          let a := mkIdent (← mkFreshUserName `a)
+          ctorArgs := ctorArgs.push a
+          rhsArgs := rhsArgs.push <| ← mkArg xs[ctorInfo.numParams + i]! a
+        patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*))
+        let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)}))
+        let rhs : Term ←
+          mkAppNTerm (← `(Expr.const $(quote ctorInfo.name) [$levels,*])) rhsArgs
+        `(matchAltExpr| | $[$patterns:term],* => $rhs)
+      alts := alts.push alt
+    return alts
+
+/-- Create the body of the `toTypeExpr` function for the `ToExpr` instance.
+Calls `toExpr` and `toTypeExpr` to the arguments to the type constructor. -/
+def mkToTypeExpr (argNames : Array Name) (indVal : InductiveVal) : TermElabM Term := do
+  let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)}))
+  forallTelescopeReducing indVal.type fun xs _ => do
+    let mut args : Array Term := #[]
+    for i in [:xs.size] do
+      let x := xs[i]!
+      let a := mkIdent argNames[i]!
+      if ← Meta.isType x then
+        args := args.push <| ← `(toTypeExpr $a)
+      else
+        args := args.push <| ← `(toExpr $a)
+    mkAppNTerm (← `((Expr.const $(quote indVal.name) [$levels,*]))) args
+
+/--
+For mutually recursive inductive types, the strategy is to have local `ToExpr` instances in scope
+for each of the inductives when defining each instance.
+This way, each instance can freely use `toExpr` and `toTypeExpr` for each of the other types.
+
+Note that each instance gets its own definition of each of the others' `toTypeExpr` fields.
+(This is working around the fact that the `Deriving.Context` API assumes
+that each instance in mutual recursion only has a single auxiliary definition.
+There are other ways to work around it, but `toTypeExpr` implementations
+are very simple, so duplicating them seemed to be OK.) -/
+def mkLocalInstanceLetDecls (ctx : Deriving.Context) (argNames : Array Name) :
+    TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do
+  let mut letDecls := #[]
+  for i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]!
+    let auxFunName   := ctx.auxFunNames[i]!
+    let currArgNames ← mkInductArgNames indVal
+    let numParams    := indVal.numParams
+    let currIndices  := currArgNames[numParams:]
+    let binders      ← mkImplicitBinders currIndices
+    let argNamesNew  := argNames[:numParams] ++ currIndices
+    let indType      ← mkInductiveApp indVal argNamesNew
+    let instName     ← mkFreshUserName `localinst
+    let toTypeExpr   ← mkToTypeExpr argNames indVal
+    let letDecl      ← `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* :
+                            ToExpr $indType :=
+                          { toExpr := $(mkIdent auxFunName), toTypeExpr := $toTypeExpr })
+    letDecls := letDecls.push letDecl
+  return letDecls
+
+/-- Fix the output of `mkInductiveApp` to explicitly reference universe levels. -/
+def fixIndType (indVal : InductiveVal) (t : Term) : TermElabM Term :=
+  match t with
+  | `(@$f $args*) =>
+    let levels := indVal.levelParams.toArray.map mkIdent
+    `(@$f.{$levels,*} $args*)
+  | _ => throwError "(internal error) expecting output of `mkInductiveApp`"
+
+/-- Make `ToLevel` instance binders for all the level variables. -/
+def mkToLevelBinders (indVal : InductiveVal) : TermElabM (TSyntaxArray ``instBinderF) := do
+  indVal.levelParams.toArray.mapM (fun u => `(instBinderF| [ToLevel.{$(mkIdent u)}]))
+
+open TSyntax.Compat in
+/-- Make a `toExpr` function for the given inductive type.
+The implementations of each `toExpr` function for a (mutual) inductive type
+are given as top-level private definitions.
+These end up being assembled into `ToExpr` instances in `mkInstanceCmds`.
+For mutual inductive types,
+then each of the other types' `ToExpr` instances are provided as local instances,
+to wire together the recursion (this necessitates these auxiliary definitions being `partial`). -/
+def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do
+  let auxFunName := ctx.auxFunNames[i]!
+  let indVal     := ctx.typeInfos[i]!
+  let header     ← mkToExprHeader indVal
+  let mut body   ← mkToExprBody header indVal auxFunName
+  if ctx.usePartial then
+    let letDecls ← mkLocalInstanceLetDecls ctx header.argNames
+    body ← mkLet letDecls body
+  -- We need to alter the last binder (the one for the "target") to have explicit universe levels
+  -- so that the `ToLevel` instance arguments can use them.
+  let addLevels binder :=
+    match binder with
+    | `(bracketedBinderF| ($a : $ty)) => do `(bracketedBinderF| ($a : $(← fixIndType indVal ty)))
+    | _ => throwError "(internal error) expecting inst binder"
+  let binders := header.binders.pop
+    ++ (← mkToLevelBinders indVal)
+    ++ #[← addLevels header.binders.back]
+  let levels := indVal.levelParams.toArray.map mkIdent
+  if ctx.usePartial then
+    `(private partial def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :
+        Expr := $body:term)
+  else
+    `(private def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* :
+        Expr := $body:term)
+
+/-- Create all the auxiliary functions using `mkAuxFunction` for the (mutual) inductive type(s).
+Wraps the resulting definition commands in `mutual ... end`. -/
+def mkMutualBlock (ctx : Deriving.Context) : TermElabM Syntax := do
+  let mut auxDefs := #[]
+  for i in [:ctx.typeInfos.size] do
+    auxDefs := auxDefs.push (← mkAuxFunction ctx i)
+  `(mutual $auxDefs:command* end)
+
+open TSyntax.Compat in
+/-- Assuming all of the auxiliary definitions exist, create all the `instance` commands
+for the `ToExpr` instances for the (mutual) inductive type(s). -/
+def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) :
+    TermElabM (Array Command) := do
+  let mut instances := #[]
+  for i in [:ctx.typeInfos.size] do
+    let indVal       := ctx.typeInfos[i]!
+    if typeNames.contains indVal.name then
+      let auxFunName   := ctx.auxFunNames[i]!
+      let argNames     ← mkInductArgNames indVal
+      let binders      ← mkImplicitBinders argNames
+      let binders      := binders ++ (← mkInstImplicitBinders ``ToExpr indVal argNames)
+      let binders      := binders ++ (← mkToLevelBinders indVal)
+      let indType      ← fixIndType indVal (← mkInductiveApp indVal argNames)
+      let toTypeExpr   ← mkToTypeExpr argNames indVal
+      let levels       := indVal.levelParams.toArray.map mkIdent
+      let instCmd ← `(instance $binders:implicitBinder* : ToExpr $indType where
+                        toExpr := $(mkIdent auxFunName).{$levels,*}
+                        toTypeExpr := $toTypeExpr)
+      instances := instances.push instCmd
+  return instances
+
+/-- Returns all the commands generated by `mkMutualBlock` and `mkInstanceCmds`. -/
+def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
+  let ctx ← mkContext "toExpr" declNames[0]!
+  let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx declNames)
+  trace[Elab.Deriving.toExpr] "\n{cmds}"
+  return cmds
+
+/-- The main entry point to the `ToExpr` derive handler. -/
+def mkToExprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
+  if (← declNames.allM isInductive) && declNames.size > 0 then
+    let cmds ← liftTermElabM <| mkToExprInstanceCmds declNames
+    cmds.forM elabCommand
+    return true
+  else
+    return false
+
+initialize
+  registerDerivingHandler ``Lean.ToExpr mkToExprInstanceHandler
+  registerTraceClass `Elab.Deriving.toExpr
+
+end QuoteLight.Deriving.ToExpr
diff --git a/Tactics/QuoteLight/ToExpr.lean b/Tactics/QuoteLight/ToExpr.lean
new file mode 100644
index 00000000..863862eb
--- /dev/null
+++ b/Tactics/QuoteLight/ToExpr.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+Source: https://github.com/leanprover-community/mathlib4/blob/8d6f380fde8631e39a62b5a009b2ffec2eb3c17f/Mathlib/Tactic/ToExpr.lean
+-/
+import Tactics.QuoteLight.DeriveToExpr
+
+/-! # `ToExpr` instances for Mathlib
+
+This module should be imported by any module that intends to define `ToExpr` instances.
+It provides necessary dependencies (the `Lean.ToLevel` class) and it also overrides the instances
+that come from core Lean 4 that do not handle universe polymorphism.
+(See the module `Lean.ToExpr` for the instances that are overridden.)
+
+In addition, we provide some additional `ToExpr` instances for core definitions.
+-/
+
+section override -- Note: this section uses `autoImplicit` pervasively
+namespace Lean
+
+attribute [-instance] Lean.instToExprOption
+
+set_option autoImplicit true in
+deriving instance ToExpr for Option
+
+attribute [-instance] Lean.instToExprList
+
+set_option autoImplicit true in
+deriving instance ToExpr for List
+
+attribute [-instance] Lean.instToExprArray
+
+universe u in
+instance {α : Type u} [ToExpr α] [ToLevel.{u}] : ToExpr (Array α) :=
+  let type := toTypeExpr α
+  { toExpr     := fun as => mkApp2 (mkConst ``List.toArray [toLevel.{u}]) type (toExpr as.toList)
+    toTypeExpr := mkApp (mkConst ``Array [toLevel.{u}]) type }
+
+attribute [-instance] Lean.instToExprProd
+
+set_option autoImplicit true in
+deriving instance ToExpr for Prod
+
+deriving instance ToExpr for System.FilePath
+
+end Lean
+end override
+
+namespace Mathlib
+open Lean
+
+set_option autoImplicit true in
+deriving instance ToExpr for ULift
+
+universe u in
+/-- Hand-written instance since `PUnit` is a `Sort` rather than a `Type`. -/
+instance [ToLevel.{u}] : ToExpr PUnit.{u+1} where
+  toExpr _ := mkConst ``PUnit.unit [toLevel.{u+1}]
+  toTypeExpr := mkConst ``PUnit [toLevel.{u+1}]
+
+deriving instance ToExpr for String.Pos
+deriving instance ToExpr for Substring
+deriving instance ToExpr for SourceInfo
+deriving instance ToExpr for Syntax.Preresolved
+deriving instance ToExpr for Syntax
+
+open DataValue in
+/-- Core of a hand-written `ToExpr` handler for `MData`.
+Uses the `KVMap.set*` functions rather than going into the internals
+of the `KVMap` data structure. -/
+private def toExprMData (md : MData) : Expr := Id.run do
+  let mut e := mkConst ``MData.empty
+  for (k, v) in md do
+    let k := toExpr k
+    e := match v with
+          | ofString v => mkApp3 (mkConst ``KVMap.setString) e k (mkStrLit v)
+          | ofBool v   => mkApp3 (mkConst ``KVMap.setBool) e k (toExpr v)
+          | ofName v   => mkApp3 (mkConst ``KVMap.setName) e k (toExpr v)
+          | ofNat v    => mkApp3 (mkConst ``KVMap.setNat) e k (mkNatLit v)
+          | ofInt v    => mkApp3 (mkConst ``KVMap.setInt) e k (toExpr v)
+          | ofSyntax v => mkApp3 (mkConst ``KVMap.setSyntax) e k (toExpr v)
+  return e
+
+instance : ToExpr MData where
+  toExpr := toExprMData
+  toTypeExpr := mkConst ``MData
+
+deriving instance ToExpr for FVarId
+deriving instance ToExpr for MVarId
+deriving instance ToExpr for LevelMVarId
+deriving instance ToExpr for Level
+deriving instance ToExpr for BinderInfo
+deriving instance ToExpr for Literal
+deriving instance ToExpr for Expr
+
+end Mathlib
diff --git a/Tactics/QuoteLight/ToLevel.lean b/Tactics/QuoteLight/ToLevel.lean
new file mode 100644
index 00000000..33967ca0
--- /dev/null
+++ b/Tactics/QuoteLight/ToLevel.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+Source: https://github.com/leanprover-community/mathlib4/blob/8d6f380fde8631e39a62b5a009b2ffec2eb3c17f/Mathlib/Tactic/ToLevel.lean
+-/
+import Lean
+
+/-! # `ToLevel` class
+
+This module defines `Lean.ToLevel`, which is the `Lean.Level` analogue to `Lean.ToExpr`.
+
+**Warning:** Import `Mathlib.Tactic.ToExpr` instead of this one if you are writing `ToExpr`
+instances. This ensures that you are using the universe polymorphic `ToExpr` instances that
+override the ones from Lean 4 core.
+
+-/
+
+namespace Lean
+
+/-- A class to create `Level` expressions that denote particular universe levels in Lean.
+`Lean.ToLevel.toLevel.{u}` evaluates to a `Lean.Level` term representing `u` -/
+class ToLevel.{u} where
+  /-- A `Level` that represents the universe level `u`. -/
+  toLevel : Level
+  /-- The universe itself. This is only here to avoid the "unused universe parameter" error. -/
+  univ : Type u := Sort u
+export ToLevel (toLevel)
+
+instance : ToLevel.{0} where
+  toLevel := .zero
+
+universe u v
+
+instance [ToLevel.{u}] : ToLevel.{u+1} where
+  toLevel := .succ toLevel.{u}
+
+/-- `ToLevel` for `max u v`. This is not an instance since it causes divergence. -/
+def ToLevel.max [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{max u v} where
+  toLevel := .max toLevel.{u} toLevel.{v}
+
+/-- `ToLevel` for `imax u v`. This is not an instance since it causes divergence. -/
+def ToLevel.imax [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{imax u v} where
+  toLevel := .imax toLevel.{u} toLevel.{v}
+
+end Lean