[Why3-club] how to pass arguments to commands in IDE 1.2.0

Jean-Jacques Levy jean-jacques.levy at inria.fr
Fri Feb 22 13:50:09 CET 2019


Dear Friends,

in why3.1.2.0, I cannot succeed in passing an argument to command in line 0/0/0 !!
-------------------------
goal list_simpl_r :
  forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2
-------------------------
Following hypothesis was not found: l1 

Transformation failed: 
induction_arg_ty_lex  l1

induction_arg_ty_lex
type: lsymbol -> list task
induction_arg_ty_lex <ls> performs induction_ty_lex on ls.
-------------------------
In why3.0.88.3, it was simple induction_ty_lex on ‘l1’ with keyword "induction"
and if induction is done on l2, then generalization is lost.

Pls help ! Cheers -JJ-



More information about the Why3-club mailing list