INDPROP.归纳定义命题.案例研究：正则表达式
Case Study: Regular Expressions
ev属性提供了一个简单的例子来说明归纳定义和对其进行推理的基本技术，但它并不十分令人兴奋——毕竟，它相当于我们已经看到的两个非归纳均匀度定义，并且似乎没有提供任何具体的好处。
为了更好地理解归纳定义的威力，我们现在展示如何使用它们来模拟计算机科学中的一个经典概念：正则表达式。
正则表达式是一种描述字符串集的简单语言。其语法定义如下：
【学习】函数语言程序设计 文章被收录于专栏
函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】
投递深圳同为数码等公司10个岗位