Update dependent_type_theory.md (leanprover#70)

The `Nat` does not need to be here if this is intended to show that Lean can infer types sometimes.
FormalMathematicsLab · Mar 1, 2024 · 048b6bb · 048b6bb
1 parent 5f77cc5
commit 048b6bb
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/dependent_type_theory.md b/dependent_type_theory.md
@@ -292,8 +292,8 @@ from an expression as follows:
 ```lean
 #check fun (x : Nat) => x + 5   -- Nat → Nat
 #check λ (x : Nat) => x + 5     -- λ and fun mean the same thing
-#check fun x : Nat => x + 5     -- Nat inferred
-#check λ x : Nat => x + 5       -- Nat inferred
+#check fun x => x + 5     -- Nat inferred
+#check λ x => x + 5       -- Nat inferred
 ```
 
 You can evaluate a lambda function by passing the required parameters: