Changeset 1920 for src/Clight/Csyntax.ma
- Timestamp:
- May 8, 2012, 11:16:18 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csyntax.ma
r1872 r1920 208 208 | LSdefault: statement → labeled_statements 209 209 | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements. 210 211 let 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 ≝ 216 match 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 ]. 210 220 211 221 let rec statement_ind2
Note: See TracChangeset
for help on using the changeset viewer.