search

namme-anetten / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

definitionsToImpl and magicImplName #58

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
(This issue is for documentation purposes, I don't fully understand the point 
of these functions yet. They just look very odd.)

In ProofState.Edition.Scope, there is a function called |definitionsToImpl| 
that filters the definitions in scope which name is |magicImplName|. This is an 
abuse of the naming scheme, with the risks you can expect.

Maybe there is no cleaner solution for the moment, or maybe (that's what I hope 
for) we can clean this up when we have a high-level system. Anyway, it's worth 
documenting here.

Original issue reported on code.google.com by pedag...@gmail.com on 26 Aug 2010 at 4:43

GoogleCodeExporter commented 9 years ago 
The point of definitionsToImpl is to determine the local context for 
elimination with a motive: it allows us to drop all parameters above the 
implementation of a 'let' definition. The function, or something like it, may 
also be useful for relabelling (issue 23). Using the name of the goal to 
identify the relevant definition is a cheap and unproblematic hack; we could 
store a flag in the proof state if we wanted to be more principled.

Original comment by adamgundry on 31 Aug 2010 at 2:12