Changeset 1920 for src/common/AST.ma


Ignore:
Timestamp:
May 8, 2012, 11:16:18 AM (8 years ago)
Author:
campbell
Message:

Most of the labelling simulation. Still need to sort out switch statements
and function calls.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1882 r1920  
    207207] qed.
    208208
     209lemma intsize_eq_elim_false : ∀A,sz,sz',P,p,f,d.
     210  sz ≠ sz' →
     211  intsize_eq_elim A sz sz' P p f d = d.
     212#A * * // #P #p #f #d * #H cases (H (refl ??))
     213qed.
    209214
    210215(* A type for the integers that appear in the semantics. *)
Note: See TracChangeset for help on using the changeset viewer.