[Agda] refuting with rewrite

[gallais at EnsL.org]

Hi Brandon,

you should write:

fun : (b : Bool) → So b → b ≡ false → ⊥
fun .false () refl

[refl] is the only constructor for [≡] and the dotted pattern [.false]
indicates that this value is forced by the context (the fact that the
equality has been pattern-match against). This way the typechecker
can see that your second argument is supposed to be of type
[So false] which is impossible.

Cheers,

--
guillaume



On 9 March 2011 04:29, Brandon Moore <brandon_m_moore at yahoo.com> wrote:
> Why doesn't this go through? It seems pointless to "with" on a trivial value
> so the refutation can be written on the next line.
>
> module test where
> open import Relation.Binary.PropositionalEquality
> open import Data.Bool
> open import Data.Empty
>
> data So : Bool → Set where oh : So true
>
> fun : (b : Bool) → So b → b ≡ false → ⊥
> fun b () eq rewrite eq
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>