Skip to content

Commit 1718b58

Browse files
committed
chore: fix a typo in a doc comment
1 parent 39cbe04 commit 1718b58

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Compiler/LCNF/CompilerM.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,7 @@ inductive NormFVarResult where
213213
fvar (fvarId : FVarId)
214214
| /--
215215
Free variable has been erased. This can happen when instantiating polymorphic code
216-
with computationally irrelant stuff. -/
216+
with computationally irrelevant stuff. -/
217217
erased
218218
deriving Inhabited
219219

0 commit comments

Comments
 (0)