Changeset 3534 for LTS


Ignore:
Timestamp:
Mar 16, 2015, 1:02:06 PM (5 years ago)
Author:
pellitta
Message:

abitato record di tipo instr_params

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3533 r3534  
    130130#H1 >H1 #H2 >H2 normalize %]qed.
    131131
     132lemma expr_eq_equality:∀e1,e2.expr_eq e1 e2=true ↔ e1=e2.
     133#e1 #e2 % [@expr_eq_equality_one|@expr_eq_equality_two] qed.
     134
    132135(*
    133136lemma expr_eq_equality_two':∀e1,e2.e1≠e2→ expr_eq e1 e2=false.
     
    167170|#c' normalize * %] qed.
    168171
    169 lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
     172lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
    170173#c1 #c2 % [2: * @condition_eq_sym
    171174| lapply c2 -c2 elim c1 normalize
     
    202205*)
    203206
    204 (*
    205207inductive loop_i:Type[0]≝lWhile: loop_i.
    206208definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true.
    207209lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
    208210cases l1 cases l2 % #_ % qed.
    209 *)
    210211
    211212(*
     
    223224|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    224225|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    225 |@(mk_DeqSet nat neqb neqb_true_to_eq)
    226 |@(mk_DeqSet nat neqb neqb_true_to_eq)].qed.
     226|@(mk_DeqSet expr expr_eq expr_eq_equality)
     227|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
    227228
    228229(* | IfThenElse: condition → command → command → command*)
Note: See TracChangeset for help on using the changeset viewer.