Changeset 1672 for src/Clight/Csem.ma


Ignore:
Timestamp:
Feb 1, 2012, 4:16:06 PM (7 years ago)
Author:
campbell
Message:

Matita now generates a couple of inversion lemmas that were manually
proved before.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r1545 r1672  
    722722  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
    723723  ].
    724 
     724(*
    725725inverter eval_expr_inv_ind for eval_expr : Prop.
    726 
     726*)
    727727let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
    728728  (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
     
    744744ninverter eval_lvalue_inv_ind for eval_lvalue : Prop.
    745745*)
    746 
     746(*
    747747definition eval_lvalue_inv_ind :
    748748  ∀x1: genv.
     
    793793| *: skip
    794794] qed.
    795 
     795*)
    796796let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
    797797  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
Note: See TracChangeset for help on using the changeset viewer.