\documentclass{article}
\usepackage[a4paper,margin=1in]{geometry}
\usepackage{leantex}

% Generated by: leantex build examples/minimal/minimal.tex
\input{leantex.generated.tex}

\title{LeanTeX Minimal Example}
\date{}

\begin{document}
\maketitle

This document has two Lean snippets. The first should pass and show an info message.

\begin{lean}[name=ok,show=both]
#check Nat.succ
example : 1 + 1 = 2 := by decide
\end{lean}

This one intentionally fails so you can see snippet-local errors.

\begin{lean}[name=bad,show=both]
example : 1 + 1 = 3 := by
  decide
\end{lean}

\section*{Whole Extracted File}

\totalinfoview

\end{document}