Ignore:
Timestamp:
Dec 2, 2011, 1:02:08 PM (8 years ago)
Author:
campbell
Message:

More on RTLabs structured traces.
Fixed mistake in structure trace definition that made it unhabitable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r1545 r1583  
    549549  ?*)
    550550.
     551
     552lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
     553  find_funct Genv F ge v = Some F f →
     554  ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset)  ∧ find_funct_ptr Genv F ge b = Some F f.
     555#F #ge *
     556[ #f #E normalize in E; destruct
     557| #sz #i #f #E normalize in E; destruct
     558| #f #fn #E normalize in E; destruct
     559| #r #f #E normalize in E; destruct
     560| * #pty #b #c * #off #f #E normalize in E;
     561  cases off in E ⊢ %; [ 2,3: #x ]
     562  #E normalize in E; destruct
     563  %{pty} %{b} %{c} % // @E
     564] qed.
     565
    551566(*
    552567##[ #A B C transf p b f; elim p; #fns main vars;
Note: See TracChangeset for help on using the changeset viewer.