I want to capture type validity in my Expr
definition, and there is a problem when I'm defining Add
, which is expected to be followed by Decimal
or Whole
arguments, but I don't know how to pattern match them both. following is my trials:
1st trial :
data DataType = Text | Decimal | Whole
data Expr : DataType -> Type where
Add : (Expr Decimal) -> (Expr Decimal) -> Expr Decimal
Add : (Expr Whole) -> (Expr Whole) -> Expr Whole
2nd trial:
data DataType = Text | Decimal | Whole
data Expr : DataType -> Type where
Add : (Expr ty) -> (Expr ty) -> Expr ty
3rd trial:
data DataType = Text | Decimal | Whole
data Expr : DataType -> Type where
Add : (Expr ty@(Decimal | Whole)) -> (Expr ty) -> Expr ty
In 1st trial, I'm told that I can't define Add
twice. And in 2nd trial, I don't know how to add the constriant that ty
must be one of Decimal
and Whole
. And 3rd trial is using some imaginary syntax which is not supported yet..