diff --git a/.gitignore b/.gitignore index 3c2ebb6..9b6fc48 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ /.lake .directory +qr-code.png diff --git a/Lean Talk SP24/basics.lean b/Lean Talk SP24/basics.lean index b08c430..ae371f9 100644 --- a/Lean Talk SP24/basics.lean +++ b/Lean Talk SP24/basics.lean @@ -13,6 +13,8 @@ open Nat def f (x : ℕ) := x + 3 +#eval f 5 + #check f -- These are propositions, of type `Prop`. diff --git a/lake-manifest.json b/lake-manifest.json index ccdf972..e75a757 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "328b7ecbc986507635abf725bbed4da70e418298", + "rev": "e415c3ba4d1e59e5af6d0b9b4f71797f97cad62a", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,