We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent b3c5575 commit 608cbe1Copy full SHA for 608cbe1
1 file changed
Cslib/Languages/CombinatoryLogic/Defs.lean
@@ -40,7 +40,7 @@ namespace Cslib
40
41
/-- An SKI expression is built from the primitive combinators `S`, `K` and `I`, and application. -/
42
inductive SKI where
43
- /-- `S`-combinator, with semantics $λxyz.xz(yz) -/
+ /-- `S`-combinator, with semantics $λxyz.xz(yz)$ -/
44
| S
45
/-- `K`-combinator, with semantics $λxy.x$ -/
46
| K
0 commit comments