Zulip Chat Archive

Stream: general

Topic: GADT trouble


Alice Laroche (Jan 24 2022 at 14:14):

I have this :

inductive regex : nat -> Type*
| emp         : regex 0
| chr         : char -> regex 0
| group       : nat -> regex n -> regex (n + 1)
| alt   (m n) : regex m -> regex n -> regex (m + n)
| conct (m n) : regex m -> regex n -> regex (m + n)
open regex

instance {n' : nat } : has_sizeof (regex n') :=

  λreg, match reg with
      | alt m n r r' := 0
      | _ := 0
      end

And i have this error :

type mismatch at application
  _match (alt m n r r')
term
  alt m n r r'
has type
  regex (m + n) : Type ?
but is expected to have type
  regex n' : Type ?

I understand why, but i don't know how to fix this

Zhanrong Qiao (Jan 24 2022 at 14:55):

You can match on both n' and reg:

instance {n' : nat} : has_sizeof (regex n') :=
  λ reg,
    match n', reg with
    | _, emp            := 0
    | _, chr c          := 0
    | _, group n r      := 0
    | _, alt m n r r'   := 0
    | _, conct m n r r' := 0
    end

This is called "dependent pattern matching"

Alice Laroche (Jan 24 2022 at 15:03):

Thanks


Last updated: Dec 20 2023 at 11:08 UTC