The Coq mailing list

[Liang Dou <ldou.ecnu AT gmail.com>]

Hi , all
   We have an inductive definition "execute" and we get the error for coq:

Non strictly positive occurrence of "execute" in
 "forall s : state,
  state ->
  forall (l l' : state) (a : event),
  (forall s'0 : state, ~ execute s (a :: nil) s'0) ->
  prefix s l = true -> execute l (a :: nil) l'".

=======================================
Definition event:=string.
Definition state:=string.
Definition action:=list event.

Inductive execute: state -> action -> state  ->Prop :=
|OR1: forall  (s s' l l' : state) ( a : event),
      (forall s', ~ (execute s (a::nil) s')) ->
      prefix s l = true ->
      execute l (a::nil) l' .


could someone tell ue how to fix it?


3X~~!!