Skip to content

update mdgen and hide implementation detail #165

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

update mdgen and hide implementation detail #165

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 13 additions & 3 deletions lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,21 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
"rev": "47f0ce028df42a72dc5d55e40bd4c1921a7f98bd",
"name": "mdgen",
"manifestFile": "lake-manifest.json",
"inputRev": "v1.3.0",
"inputRev": "1.11.0",
"inherited": false,
"configFile": "lakefile.lean"}],
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "c53b3371dd0fe5f3dd75a2df543c3550e246465a",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "«lean4-metaprogramming-book»",
"lakeDir": ".lake"}
2 changes: 1 addition & 1 deletion lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ lean_lib «lean4-metaprogramming-book» where
globs := #[Glob.one `cover, Glob.submodules `extra, Glob.submodules `main, Glob.submodules `solutions]

require mdgen from git
"https://github.com/Seasawher/mdgen" @ "v1.3.0"
"https://github.com/Seasawher/mdgen" @ "1.11.0"

require "leanprover-community" / "batteries" @ git "main"

Expand Down
4 changes: 2 additions & 2 deletions lean/main/01_intro.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,14 +128,14 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
logInfo "success"
catch | _ => throwError "failure"

/-- info: success -/
/-⋆-//-- info: success -/
#guard_msgs in --#
#assertType 5 : Nat

-- don't display names of metavariables
set_option pp.mvars false in

/--
/-⋆-//--
error: type mismatch
[]
has type
Expand Down
2 changes: 1 addition & 1 deletion lean/main/09_tactics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ We start by simply declaring the tactic with no implementation:

syntax "custom_tactic" : tactic

/-- error: tactic 'tacticCustom_tactic' has not been implemented -/
/-⋆-//-- error: tactic 'tacticCustom_tactic' has not been implemented -/
#guard_msgs in --#
example : 42 = 42 := by
custom_tactic
Expand Down
4 changes: 2 additions & 2 deletions lean/solutions/05_syntax.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,11 @@ syntax "yellow" : tactic

#check_failure good morning -- the syntax parsing stage works

/-- error: elaboration function for 'commandHello' has not been implemented -/
/-⋆-//-- error: elaboration function for 'commandHello' has not been implemented -/
#guard_msgs in --#
hello -- the syntax parsing stage works

/-- error: tactic 'tacticYellow' has not been implemented -/
/-⋆-//-- error: tactic 'tacticYellow' has not been implemented -/
#guard_msgs in --#
example : 2 + 2 = 4 := by
yellow -- the syntax parsing stage works
Expand Down