[Agda] Impossible proofs about where blocks?

[Andreas Abel]

In the back of my mind I remember from some Agda meeting talk that

   bla : _
   bla = ...
     where blurp = ...

allows one to access blurp as

   bla.blurp

But that does not seem to be the case...

@Ulf:  Did such a feature exist at some time?

Cheers,
Andreas

On 16.06.11 1:26 AM, Daniel Peebles wrote:
> Let's say I'm writing a proof with a goal type of:
>
> Goal: (fromℕ
>         (peanoInduction (λ {x'} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)
>          (toPeano (x ∷ xs)))
>         | (.Data.Digit._.helper 0
>            (peanoInduction (λ {x'} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)
>             (toPeano (x ∷ xs)))
>            (peanoInduction (λ {x'} _ → ℕ) 0 (λ {.x} {.m} → Nsuc)
>             (toPeano (x ∷ xs)))
>    ...
>
> Note that it will not proceed in normalizing the goal type unless I can
> match on the result of the expression after the pipe. Unfortunately,
> said expression lives within a where block in a module that's out of my
> control, so I can't see it at all, to proceed on the proof. As far as I
> can understand, assuming there aren't completely different approaches to
> the proof, this makes my proof actually impossible. Am I correct?
>
> Now, the ._.helper notation looks like the helper is secretly living
> inside an anonymous module that the where block created. Given the
> recent change that made datatypes into modules, would it be worthwhile
> or problematic to make all value declarations with where blocks into
> explicit modules as well, so that we can open them and prove things
> about whatever happened inside? Would this cause problems in other ways?
>
> Even if my suggestion isn't valid, it seems like it'd be good to have a
> good answer for this kind of situation. Or is there already some
> solution that I'm missing?
>
> Thanks,
> Dan
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/