[Agda] pattern matching on records

[Amr Sabry]

Ah. Obvious in retrospect. Thank you!!!

--Amr

Twan van Laarhoven <twanvl at gmail.com> wrote:

> If I write
> 
>     simplify : {t₁ t₂ : U•} → (c₁ : t₁ ⟷ t₂) → (t₂ ⟷ t₁)
>     simplify swap1₊ = swap2₊
>     simplify swap2₊ = swap1₊
> 
> then agda colors this yellow, because there are unsolved metas. In
> particular, the type of swap1₊ fixes ∣ t₁ ∣, ∣ t₂ ∣ and (• t₁), but not (•
> t₂).
> 
> These problems go away if you change _⟷_ to
> 
>     data _⟷_ : U• → U• → Set where
>       swap1₊  : ∀ {∣t₁∣ ∣t₂∣ •t₁} → •[ PLUS ∣t₁∣ ∣t₂∣ , inj₁ •t₁ ] ⟷
>                                   •[ PLUS ∣t₂∣ ∣t₁∣ , inj₂ •t₁ ]
>       swap2₊  : ∀ {∣t₁∣ ∣t₂∣ •t₂} → •[ PLUS ∣t₁∣ ∣t₂∣ , inj₂ •t₂ ] ⟷
>                                   •[ PLUS ∣t₂∣ ∣t₁∣ , inj₁ •t₂ ]
> 
> 
> Twan
> 
> On 2014-06-30 17:59, Amr Sabry wrote:
> > How does one do "deep" pattern matches on records involving dot
> > patterns. Is it even possible? In the attached program 'simplify' should
> > have the "obvious" definition commented at the bottom but nothing I can
> > write will allow Agda to infer or even pattern match on the implicit
> > arguments. Any help would be appreciated. Thanks. --Amr
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda