[Agda] signature for `with' branch

[Sergei Meshveliani]

On Wed, 2017-03-01 at 08:14 +0100, Ulf Norell wrote:
> The problem you have is that you can't talk about the aux function.
> You can use 
> named where modules to make it visible which enables
> proving the relevant lemma for it:
> 
> 
> open import Function using (flip)
> open import Relation.Binary using (Rel; Tri; StrictTotalOrder)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
> open import Data.Empty
> 
> 
> module _ {α α= α<} (sto : StrictTotalOrder α α= α<)
>   where
>   open StrictTotalOrder sto using (_≈_; _<_; compare)
>                             renaming (Carrier to C)
>   _>_ = flip _<_
>   open Tri
> 
> 
>   min : (x y : C) → C
>   min x y = aux (compare x y)
>     module min where
>           aux : Tri (x < y) (x ≈ y) (x > y) → C
>           aux (tri< _ _ _) = x
>           aux (tri≈ _ _ _) = x
>           aux (tri> _ _ _) = y
> 
> 
>   lemma-aux : ∀ {x y} → x < y → (t : Tri (x < y) (x ≈ y) (x > y)) → 
>                                                  min.aux x y t ≡ x
>   lemma-aux x<y (tri< a ¬b ¬c) = _≡_.refl
>   lemma-aux x<y (tri≈ ¬a b ¬c) = _≡_.refl
>   lemma-aux x<y (tri> ¬a ¬b c) = ⊥-elim (¬a x<y)
> 
> 
>   lemma :  ∀ x y → x < y → min x y ≡ x
>   lemma x y x<y = lemma-aux x<y (compare x y)
> 

Thank you. 
It is nice to know that `with' and `case_of_' can be replaced.


------
Sergei