[Agda] Type and termination checking around with clauses

[Ulf Norell]

On Wed, Apr 30, 2008 at 10:39 PM, Nils Anders Danielsson <
nils.anders.danielsson at gmail.com> wrote:

> On Wed, Apr 30, 2008 at 6:28 PM, Peter Berry <pwberry at gmail.com> wrote:
> >
> >  Atom : Bool -> Set
> >  Atom true  = ⊤
> >  Atom false = ⊥
>
> > _<=_ : ℕ -> ℕ -> Bool
> >  Z   <= _   = true
> >  S _ <= Z   = false
> >  S n <= S m = n <= m
> >
> >  -- contrived version, I know it can be done more simply!
> >  trans : {n m o : ℕ} -> Atom (n <= m) -> Atom (m <= o) -> Atom (n <= o)
> >  trans {Z}               triv _ = triv
> >  trans {S _} {Z}         () _
> >  trans {S _} {S _} {Z}   _ ()
> >  trans {S n} {S m} {S o} p q with n <= m
> >  ... | false with p
> >  ...     | ()
> >  trans {S n} {S m} {S o} p q
> >     | true with m <= o
> >  ...     | true  = trans {n} {m} {o} {! !} {! !}
> >  ...     | false with q
> >  ...        | ()
>
> >  The two holes have types Atom (n <= m) and Atom (m <= o) respectively,
> >  which are clearly both equal to ⊤, but the type checker won't accept
> >  'triv' there.
>
> The goal types are not equal to ⊤, since the type checker is not aware
> of the results of your tests.


The with is supposed to make the type checker aware of the result of the
test, that's the whole point (well, maybe not the whole point). I haven't
tried the example yet, but just looking at it, it should work.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080501/713ba6ff/attachment.html