Skip to content

Commit

Permalink
Update manual.tex: Fixed way of importing autosubst
Browse files Browse the repository at this point in the history
Require Import Autosubst does not work.
  • Loading branch information
TheCodingWombat authored Aug 20, 2024
1 parent da515d5 commit 6b619c8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion manual.tex
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ \section{Tutorial}

We start by importing the \Autosubst library.
\begin{lstlisting}
Require Import Autosubst.
From Autosubst Require Import Autosubst.
\end{lstlisting}

Using de~Bruijn Syntax in Coq, the untyped lambda calculus is usually defined as shown \autoref{fig:naive-ulc-term-def}.
Expand Down

0 comments on commit 6b619c8

Please sign in to comment.