Pattern matching on structs causes TyckerException about aya-dev HOT 7 CLOSED

…you need to pattern match on x.fst, x.snd, etc.

This isn't possible in data definitions…

from aya-dev.

I think there isn't a syntax for that

from aya-dev.

You should use projections on structs.

from aya-dev.

We will now report an error for this code (instead of throwing exceptions)

from aya-dev.

But how to use projections in patterns? Sorry if this is a stupid question.

from aya-dev.

But how to use projections in patterns? Sorry if this is a stupid question.

I mean you need to pattern match on x.fst, x.snd, etc. But then you need to create new functions to pattern match on 'em. Sorry, the syntax is stupid, but we haven't decided on how to implement pattern matching expressions.

from aya-dev.

…you need to pattern match on x.fst, x.snd, etc.

This isn't possible in data definitions…

open data U2Impl (x y : Bool) : Set
  | false, false => zero
  | false, true => one
  | true, false => two
  | true, true => three

def U2 (x : BoolPair) => U2Impl x.fst x.snd

from aya-dev.