-
Hi, I try to experiment a small test. My code to run is the below.
The code prints I have three ambiguous points.
Please answer... |
Beta Was this translation helpful? Give feedback.
Answered by
yangky11
Dec 9, 2023
Replies: 1 comment
-
The
|
Beta Was this translation helpful? Give feedback.
0 replies
Answer selected by
yangky11
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
pp
is the acronym for "pretty-printed", so it's just the canonical string representation of Lean tactic state.The
id
is just a unique name ofTacticState
. Their numbers are not important as long as different states have different IDs.LeanGitRepo
doesn't havefile_path
andfull_name
. They belong toTheorem
.