[Agda] rewriting product types vs. single ctor data/record types

[Darryl McAdams]

You really ought to give an example where this distinction makes a difference.
 
- darryl


________________________________
 From: Jonathan Leivent <jleivent at comcast.net>
To: agda at lists.chalmers.se 
Sent: Sunday, August 25, 2013 1:45 PM
Subject: [Agda] rewriting product types vs. single ctor data/record types
 

I had thought that a type like

Σ[ a ∈ A ] Σ[ b ∈ B ] Σ[c ∈ C ] (D a b c)

wouldn't be any easier to use - and actually less "nice" than its 
fully-named counterpart:

record DR : Set _ where
   field
     a : A
     b : B
     c : C
     d : D a b c

or a similar single ctor inductive data type.  However, the (dependent) 
product type seems more rewritable:  if you have just "DR" as a goal, 
you can't use rewrite to help you fit things into its fields; but if you 
have that messy (dependent) product, the types of the fields (A, B, C) 
are part of the type itself - hence visible in the goal - and so can be 
targeted by rewriting.

Is there a way around this?  Is there some way to rewrite "into" the 
fields of a data/record type that appears as a goal, to achieve the same 
effect as rewriting would on a very similar product type?

-- Jonathan
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130825/ff2e5a82/attachment.html