Meta information attached to subgoals? about sml-dependent-lcf HOT 8 CLOSED

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.

from sml-dependent-lcf.

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.

from sml-dependent-lcf.

@favonia Sounds interesting! Can you give an example?

from sml-dependent-lcf.

@favonia That would be awesome.

from sml-dependent-lcf.

yes, excellent thought.

from sml-dependent-lcf.

@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?

from sml-dependent-lcf.

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.

from sml-dependent-lcf.

@favonia I was thinking about that this morning, and came to the same conclusion. It makes sense to make it part of the infrastructure.

from sml-dependent-lcf.