Coq的强制类型转换 Coercion

由于布尔谓词输出仍为bool类型，当我们需要Prop类型时，每次都需要在后面加上=true，这样就很麻烦，比如

Lemma leq11 : (1<=1) = true.

我们可以使用强制类型转换将其转换为Prop类型
在plugin.ssrbool里有这么一条命令,可以将bool类型转化为适合的三大基本类型之一

Coercion is_true : bool >-> Sortclass.

上述引理即可简写成

Lemma leq11 : 1<=1.

付师兄说还可以这样写

Coercion is_true (t:bool) := match t with 
                              |true => True 
                              |false => False end.

标签：Coq,类型转换,Coercion,Prop,Lemma,bool,类型,true
来源： https://www.cnblogs.com/lingoquandan/p/14239220.html