[Agda] Re: pattern match for LessThan'?

[Nils Anders Danielsson]

On 2016-02-02 20:20, Andreas Abel wrote:
> 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.)

You could define the following view, but I'm not quite sure why you
would want to do that:

   data View : ∀ m n → m ≤′ n → Set where
     ≤′-refl : ∀ {m} → View m m ≤′-refl
     ≤′-step : ∀ {m n} (m≤′n : m ≤′ n) → View m (suc n) (≤′-step m≤′n)

   view : ∀ {m n} (m≤′n : m ≤′ n) → View m n m≤′n
   view ≤′-refl        = ≤′-refl
   view (≤′-step m≤′n) = ≤′-step m≤′n

-- 
/NAD