[Agda] Re: pattern match for LessThan'?

[Andreas Abel]

I'd guess that if instead of Σ and ⊎ you roll your own data type with 
two constructors and suitable indices, you can get around using 'subst'. 
  (Just a hunch, have not tested it.)

Cheers, Andreas

On 02.02.2016 13:12, Kenichi Asai wrote:
> Thanks.  Yes, ⊥-elim is something that I should have considered.
> After some struggle, I came up with the following solution (attached):
>
> inv′ : {m n : ℕ} → (m≤′n : m ≤′ n) →
>        (Σ[ m≡n ∈ m ≡ n ]
>         m≤′n ≡ subst (λ n' → m ≤′ n') m≡n (≤′-refl {m})) ⊎
>        (Σ[ n' ∈ ℕ ] Σ[ sucn'≡n ∈ suc n' ≡ n ] Σ[ m≤′n' ∈ m ≤′ n' ]
>         m≤′n ≡ subst (λ n' → m ≤′ n') sucn'≡n (≤′-step m≤′n'))
> inv′ ≤′-refl = inj₁ (refl , refl)
> inv′ {n = suc n} (≤′-step m≤′n) = inj₂ (n , refl , m≤′n , refl)
>
> which uses 'subst' to adjust types.  I expect I could then use ⊥-elim
> to eliminate unnecessary cases.  Does this seem a good solution?  If
> there are any better ways, please let me know.
>
> Sincerely,
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/