<div dir="ltr"><div>There really should be a NO_ETA pragma. I made a feature request:</div><div><br></div><a href="https://code.google.com/p/agda/issues/detail?id=1536">https://code.google.com/p/agda/issues/detail?id=1536</a><br><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 2, 2015 at 9:21 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Maybe it's nicer to use if you keep the same fields:<br>
<br>
open import Data.Bool<br>
<br>
record Σ' (b : Bool) (A : Set) (B : A -> Set) : Set where<br>
inductive<br>
constructor _,_<br>
field<br>
fst : A<br>
snd : if b then (B fst) else Σ' b A B<br>
<br>
Σ = Σ' true<br>
<br>
Cheers,<br>
Andrea<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
On Tue, Jun 2, 2015 at 8:53 PM, Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br>
> On 2015-06-02 18:44, Andrea Vezzosi wrote:<br>
>><br>
>> One hacky way would be to declare them coinductive, that would disable<br>
>> eta but also pattern matching.<br>
>><br>
>> record Foo .. : Set where<br>
>> coinductive<br>
>> field<br>
>> bar : ...<br>
><br>
><br>
> Another hack:<br>
><br>
> record Σ (A : Set) (B : A → Set) : Set where<br>
> inductive<br>
> field<br>
> fst : A<br>
> snd : B fst<br>
> dummy : ⊥ → Σ A B<br>
><br>
> And another one:<br>
><br>
> Make-Agda-believe-that-the-type-is-recursive : Set → Bool → Set<br>
> Make-Agda-believe-that-the-type-is-recursive _ true = ⊤<br>
> Make-Agda-believe-that-the-type-is-recursive A false = A<br>
><br>
> record Σ (A : Set) (B : A → Set) : Set where<br>
> inductive<br>
> constructor internal-Σ-constructor<br>
> field<br>
> fst : A<br>
> snd : B fst<br>
> dummy₁ : Bool<br>
> dummy₂ : dummy₁ ≡ true<br>
> dummy₃ : Make-Agda-believe-that-the-type-is-recursive<br>
> (Σ A B) dummy₁<br>
><br>
> pattern _,_ x y = internal-Σ-constructor x y true refl _<br>
><br>
> More seriously, I think there used to be an undocumented pragma that<br>
> turned off η-equality, but it seems to have been removed.<br>
><br>
>> On Tue, Jun 2, 2015 at 6:03 PM, Thorsten Altenkirch<br>
>> <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br>
>>><br>
>>> I was just starting to use some records to restructure some code we<br>
>>> are working on and the memory goes through the roof.<br>
><br>
><br>
> Can you report this on the bug tracker? Please include the two versions<br>
> of the code (one with lower memory consumption, and one with higher).<br>
><br>
> --<br>
> /NAD<br>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>