Teal

Typeset your documents¹ directly in your interactive theorem prover! Your math gets elaborated and type-checked.

Lean syntax gets rendered pretty, with real semantic highlighting, taking type information directly from the Lean compiler.

One central aim of Teal is to be very extensible. You can very easily add custom Teal emitters for your custom syntax, for example to make integral symbols render pretty. See the section below for how.

Hello World

Add Teal as a dependency.

• For lakefile.lean: require Teal from git "https://github.com/Kiiyya/Teal"
• For lakefile.toml: Idk

In your own Lean project:

import Teal.Typst
open Teal Typst

def f (x : Nat) : Nat := x * 10

#teal[
  = Introduction
  Here you can write Teal, which is essentially a flavor of Typst slightly adapted for Lean.
  We can refer to existing symbols such as {f : Nat -> Nat}, and
  #with{z : Nat}[ -- This `#with` is special, it won't be visible in the final `*.typ` file.
    with some new unknown variable {z}, we can say that {f z} has type {Nat}:
    -- This `#block` is not special, it will simply get passed along to the final `*.typ` file:
    #block(inset: 0.8em, fill: rgb(50, 180, 198, 12), radius: 0.5em)[
      {f z : Nat}
    ]
  ]
  Here {z} is out of scope again. -- Unknown identifier `z`.
]

set_option Teal.outputPath "typst" -- This is already the default. Will output to `YourRepoRoot/typst/`. No trailing `/`.
#teal_save all

This will result in the following file:

#import "../Typst.typ": *

= Introduction
Here you can write Teal, which is essentially a flavor of Typst slightly adapted for Lean.
We can refer to existing symbols such as $#identTV[f]:#identTT[Nat]->#identTT[Nat]$, and
with some new unknown variable $#varTV[z]$, we can say that $#identTV[f]#h(0.4em)#varTV[z]$
has type $#identTT[Nat]$:

#block(inset: 0.8em, fill: rgb(50, 180, 198, 12), radius: 0.5em)[
  $#identTV[f]#h(0.4em)#varTV[z]:#identTT[Nat]$
]
Here $#identTV[z]$ is out of scope again. 

Which looks like this:

Adding custom syntax: teal_elab and teal_emit

Teal is very easily extensible. There are two key steps to adding your own syntax: elab, and emit. Let's add embedded Lean expressions via {...}:

-- Define your own syntax into either `tealFrag` or `tealBlock` syntax categories.
-- One line is made up of many `tealFrag`ments (i.e. horizontal), while a paragraph is made up
-- of many `tealBlock`s (i.e. vertical).
syntax "{" term "}" : tealFrag

-- Then, explain how your syntax elaborates.
-- If your syntax elaborates to a Lean expression, return it. If it is purely visual, return `none`.
teal_elab expectedType => `(tealFrag| { $t:term }) => do
  -- We could manipulate Lean's `LocalContext` here, which is how `#with{x:Nat}[...]` works.
  elabTerm t expectedType -- Just using Lean's `elabTerm` for `term`. Otherwise, use `elabTeal`.

-- Finally, explain how this syntax should be emitted to Typst.
-- Here, you have access to the elaborated expressions from the previous stage, so that you can do
-- proper semantic highlighting and all kinds of other fancy things.
-- You have the same power as the Lean language server, basically.
teal_emit `(tealFrag| { $t:term }) => do
  -- We can return `typst` or `typstMath` syntax categories, and Teal will handle wrapping them in
  -- math mode `$...$` or markup mode `#[...]` automatically.
  -- The `emit` descends on the syntax.
  `(typstMath| $(<- emit t))

-- And that's it! Now you can take it for a spin:
#teal[Foo {2 * x + y}.]

You can do more complicated things, such as processing match blocks, and so on.

Folder Structure

Teal is an "open" DSL. It has some basic constructs and syntax categories such as tealContent, tealBlock, tealFrag, but almost all of the syntax is defined in various places. There is no fixed grammar. Instead, we build a teal_elab command on top of Lean's KeyedDeclsAttribute. The teal_elab command is defined in /Teal/Elab.lean.

Folder structure:

• Teal/
  • Elab/
    • Elab.lean: The teal_elab command, built on top of KeyedDeclsAttribute, as well as the elabTeal dispatcher.
    • Content.lean: Defines the basic syntax categories such as tealContent, tealBlock, tealLine, tealFrag, as well as how to elaborate them.
    • ...some more modules which define Teal syntax such as headings, lists, #with{...}[...], etc.
  • Emit.lean: Target-agnostic emitter stuff.
  • Target.lean: The Teal.target option lives here, as well as the teal_target attribute to register custom targets other than Typst.
  • Teal.lean: The main #teal[...] command, as well as the environment extension which stores emitted Typst/LaTeX/etc. This is still target-agnostic.
  • Output.lean: The Teal.outputPath option and #teal_save command live here. These actually write emitted and rendered Typst/etc to files on the file system.
  • Typst/
    • Typst.lean: Defines the Typst DSL, i.e. the typst and typstMath etc syntax categories.
    • Emit.lean: The teal_emit attribute lives here, as well as the crucial emitTypst dispatcher. Despite its name, the attribute is actually specific to Typst. I would have named it teal_emit_typst but since Typst is the default anyway, it would've been too wordy.
    • Render.lean: How to map TSyntax 'typst to String.
    • Target.lean: Registers the Teal "typst" target.
    • ...and a bunch of files which provide teal_emitters.
  • Latex/ hopefully soon :) Feel free to help.

Footnotes

1. I have typeset my entire master thesis in a spagehtti version prototype of Teal. ↩