From 89997aeb57aa3a480cb1591bb40ad8b9266c7b43 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Mon, 5 Feb 2024 21:22:49 -0600 Subject: [PATCH] build: Update lean and add some gitignores --- .gitignore | 1 + Lean Talk SP24/basics.lean | 2 ++ lake-manifest.json | 2 +- 3 files changed, 4 insertions(+), 1 deletion(-) 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,