Changeset 1920 for src/Clight/Csyntax.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/Clight/Csyntax.ma

    r1872 r1920  
    208208  | LSdefault: statement → labeled_statements
    209209  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
     210
     211let rec labeled_statements_ind
     212  (P:labeled_statements → Prop)
     213  (LSd:∀s. P (LSdefault s))
     214  (LSc:∀sz,i,s,tl. P tl → P (LScase sz i s tl))
     215  ls on ls : P ls ≝
     216match ls with
     217[ LSdefault s ⇒ LSd s
     218| LScase sz i s tl ⇒ LSc sz i s tl (labeled_statements_ind P LSd LSc tl)
     219].
    210220
    211221let rec statement_ind2
Note: See TracChangeset for help on using the changeset viewer.