[Agda] Display of private things (for higher inductive types)

[Andreas Abel]

If I understand you correctly, you want to disallow matching on #I with 
the exception that I-rec is allowed.

It seems that you need something like a concept of abstract tied to a 
module, such that only functions within the module can see through the 
definitions, but not those on the outside.  Something like "protected" 
in Java.

Interesting.  Seems like a useful concept.

Cheers,
Andreas

On 26.07.2012 16:07, Guillaume Brunerie wrote:
> Hello,
>
> As some of you know, the following trick is used in homotopy type theory
> to have reduction rules for higher inductive types:
>
>  > private
>  >   data #I : Set where
>  >     #0 : #I
>  >     #1 : #I
>  >
>  > I : Set
>  > I = #I
>  >
>  > 0 : I
>  > 0 = #0
>  >
>  > 1 : I
>  > 1 = #1
>  >
>  > postulate
>  >   seg : Id 0 1
>  >
>  > I-rec : (P : I -> Set) (x0 : P 0) (x1 : P 1) (p : Id (transport P seg
> x0) x1) -> ((x : I) -> P x)
>  > I-rec P x0 x1 p #0 = x0
>  > I-rec P x0 x1 p #1 = x1
>  >
>  > -- + propositional reduction rules for [seg]
>
> The point is that the reduction
>  > I-rec P x0 x1 p 0  -->  x0
> is definitional.
>
> Now my problem is that when using C-c C-t or even C-c C-a in a goal
> involving these definitions, "I" is reduced to something ugly (and not
> even syntactically correct) like ".Interval.#I", and with more
> complicated HIT this is sometimes very annoying (and with HIT with
> parameters there is another problem, but I don't remember what it is
> right now)
>
> Is there a workaround for that? Ideally the terms "I", "0" and "1"
> should never be reduced.
>
> I tried to declare "I" abstract, but obviously the pattern matching
> defining I-rec does not work anymore.
>
> Thanks,
>
> Guillaume
>
>
>
> _______________________________________________
> 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/