Блог

Я столкнулся с сообщением об ошибке при запуске следующего кода.

 Require Import Coq.Lists.List.
Import ListNotations.

Theorem con_not_com :
  exists A (l1 l2 : list A), l1    l2 <> l2    l1.
Proof.
   exists bool [true] [false]. 
 

Мне интересно, как я могу это решить. Спасибо.

Вам нужны запятые:

 Require Import Coq.Lists.List.
Import ListNotations.

Theorem con_not_com :
  exists A (l1 l2 : list A), l1    l2 <> l2    l1.
Proof.
   exists bool, [true], [false].