Closed favonia closed 6 years ago
@favonia Sounds interesting! Can you give an example?
For example, I can know which one is the tt branch and which is the ff one, or that I am filling the motive. It can even be stacked as a trace from the root of the proof tree.
@favonia That would be awesome.
Now thinking about it, I would like to make the type polymorphic so that maybe in RedPRL/sml-redprl we can plug in Fpp.doc
.
yes, excellent thought.
@favonia Maybe this is something that can be implemented in user-land, by making the type of judgments have some annotation. Does that make sense? Or is there some aspect that we feel would work best if it was built into the core LCF infrastructure?
I realized I did not respond to your comment! I think it is better to put this into the LCF infrastructure because whether two judgments are equal should not depend on their traces.
@favonia I was thinking about that this morning, and came to the same conclusion. It makes sense to make it part of the infrastructure.
Perhaps we can allow a rule to attach ~
string option
~something option
to each subgoal.