Skip to content
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

Add set_option pp.explicit false in Weak Head Normal Form example #146

Merged
merged 2 commits into from
Sep 29, 2024
Merged

Add set_option pp.explicit false in Weak Head Normal Form example #146

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
88cad2b
Add `set_option pp.explicit false` in Weak Head Normal Form example
kpadmasola Sep 29, 2024
4ebc7ff
Addressed review comments
kpadmasola Sep 29, 2024
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
1 change: 1 addition & 0 deletions lean/main/04_metam.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -639,6 +639,7 @@ Now, here are some examples of expressions in WHNF.
Constructor applications are in WHNF (with some exceptions for numeric types):
-/

set_option pp.explicit false
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the real issue here is above on line 569, and specifically that that line should have been doing

set_option pp.explicit true in

(with the in) rather than globally changing the setting?

Could you perhaps try that instead and check whether that makes everything look correct?

Meanwhile, as someone who doesn't know much at all about metaprogramming, I find this example confusing to start off with -- the text just got finished explaining what the general form of something in WHNF is, and then here immediately starts with an example that prints differently? Naively to me it definitely seems worthwhile to explain that the pretty printer can make something look not WHNF even when it is, but starting with such an example seems weird if I follow what the text is saying.

But it does seem like the intention is to show [1] and that that's what it used to do before the change to 569, so I'm happy to merge if you take a look at the in bit above?

And thanks as usual!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Julian The change you suggested worked, thanks! PR updated.

#eval whnf' `(List.cons 1 [])
-- [1]

Expand Down
Loading