关联标签
11得票2回答
使用Coq证明可逆列表是回文。
这是我关于回文的归纳定义：Inductive pal { X : Type } : list X -> Prop := | pal0 : pal [] | pal1 : forall ( x : X ), pal [x] | pal2 : forall ( x : X ) (...
这是我关于回文的归纳定义：Inductive pal { X : Type } : list X -> Prop := | pal0 : pal [] | pal1 : forall ( x : X ), pal [x] | pal2 : forall ( x : X ) (...