Mentions légales du service

Skip to content
  • Sylvain Dailler's avatar
    Adding induction_pr.ty_lex with arguments · d42da05f
    Sylvain Dailler authored
    * Makefile.in
    Reordered Lib_transform into makefile.
    
    * src/transform/ind_itp.ml
    Adding a dependant revert transformation
    
    * src/transform/ind_itp.mli
    Adding a transformation that does a dependant revert of a list of symbols.
    
    * src/transform/induction.ml
    Adding transformation induction_ty_lex and induction_on_hyp.
    
    * src/transform/induction_pr.ml
    induction_arg_pr and inversion_arg_pr added.
    d42da05f