[Agda] rewriting product types vs. single ctor data/record types
psygnisfive at yahoo.com
Mon Aug 26 05:29:34 CEST 2013
You really ought to give an example where this distinction makes a difference.
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
record DR : Set _ where
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?
Agda mailing list
Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda