> In the dependently typed setting, it's often the case that the > "with-scrutinee" is an expression of interest precisely because it > occurs > in the *type* of the function being defined. Correspondingly, an > Epigram implementation should (and the Agda 2 implementation now does) > abstract occurrences of the expression from the type. That makes things > a bit trickier to implement, but it's just the thing you need to replace > "stuck" computations in types with actual values. The "with" construct > is what makes it possible to keep all the layers of computation in step.
Oh, I see: you use 'with' as a heuristic for guessing the motive of the inductive family elim. How do you pick which occurrences of the with-scrutinee to refine, and which to leave as a reference to the original variable? You don't always want to refine all of them, do you? -Dan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
