Regarding the proofs (and theorems) in Lean-Github
yyyhz opened this issue · 1 comments
yyyhz commented
The dataset is great! And It's nice of you to open source them.
However, I don't understand the meaning of some of these fields very well, so to prevent misunderstandings I hope you can clarify further.
For example, "start", "end", "tactic", "state_before", "state_before", "statement" and so on. With #36, I still confused about
And I wonder which one is ground truth of the cases.
objecti0n commented
start means the start position in their original file lines and token index
end means the end position in their original file lines and token index
state_before means the state in lean and state_after means the state after interacting with the tactic in lean