lean中 case怎么用
时间: 2024-10-11 22:16:12 浏览: 5
在Lean编程语言中,`case`关键字用于模式匹配,类似于其他函数式编程语言中的`match`或`switch`。它通常用于处理枚举类型、列表或其他数据结构中的值,并根据给定条件执行相应的代码块。`case`表达式的基本语法如下:
```lean
match value with
| somePattern => body1
| otherPattern => body2
| ... | defaultPattern => defaultBody
end
```
在这里:
- `value`是要匹配的数据。
- `somePattern`, `otherPattern`, 等是可能匹配的模式。
- `body1`, `body2`是当匹配到相应模式时执行的代码块。
- `defaultPattern`是可选的,如果所有模式都不匹配,则执行`defaultBody`。
例如,假设有一个颜色枚举类型`Color`,你可以这样做:
```lean
inductive Color : Type
| Red | Green | Blue
def pickColor (color : Color) : String :=
match color with
| Color.Red => "这是红色"
| Color.Green => "这是绿色"
| Color.Blue => "这是蓝色"
end
```
当你传递一个`Color`实例给`pickColor`函数时,会根据颜色匹配结果返回对应的字符串。