[Agda] agda slow

[Andrea Vezzosi]

Maybe it's nicer to use if you keep the same fields:

open import Data.Bool

record Σ' (b : Bool) (A : Set) (B : A -> Set) : Set where
  inductive
  constructor _,_
  field
    fst : A
    snd : if b then (B fst) else Σ' b A B

Σ = Σ' true

Cheers,
Andrea


On Tue, Jun 2, 2015 at 8:53 PM, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> On 2015-06-02 18:44, Andrea Vezzosi wrote:
>>
>> One hacky way would be to declare them coinductive, that would disable
>> eta but also pattern matching.
>>
>> record Foo .. : Set where
>>     coinductive
>>     field
>>        bar : ...
>
>
> Another hack:
>
>   record Σ (A : Set) (B : A → Set) : Set where
>     inductive
>     field
>       fst   : A
>       snd   : B fst
>       dummy : ⊥ → Σ A B
>
> And another one:
>
>   Make-Agda-believe-that-the-type-is-recursive : Set → Bool → Set
>   Make-Agda-believe-that-the-type-is-recursive _ true  = ⊤
>   Make-Agda-believe-that-the-type-is-recursive A false = A
>
>   record Σ (A : Set) (B : A → Set) : Set where
>     inductive
>     constructor internal-Σ-constructor
>     field
>       fst    : A
>       snd    : B fst
>       dummy₁ : Bool
>       dummy₂ : dummy₁ ≡ true
>       dummy₃ : Make-Agda-believe-that-the-type-is-recursive
>                  (Σ A B) dummy₁
>
>   pattern _,_ x y = internal-Σ-constructor x y true refl _
>
> More seriously, I think there used to be an undocumented pragma that
> turned off η-equality, but it seems to have been removed.
>
>> On Tue, Jun 2, 2015 at 6:03 PM, Thorsten Altenkirch
>> <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>>>
>>> I was just starting to use some records to restructure some code we
>>> are working on and the memory goes through the roof.
>
>
> Can you report this on the bug tracker? Please include the two versions
> of the code (one with lower memory consumption, and one with higher).
>
> --
> /NAD
>