Ignore:
Timestamp:
Jun 18, 2015, 6:33:00 PM (4 years ago)
Author:
piccolo
Message:

assembly pass in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3570 r3574  
    134134]
    135135qed.
    136 
    137 lemma nth_first : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| > n → nth_opt … n (l1 @ l2) = nth_opt … n l1.
    138 #A #l1 elim l1 [ #l2 #n normalize #H @⊥ /2/] #x #xs #IH #l2 * // #n #H @IH normalize in H; /2/
    139 qed.
    140 
    141 lemma nth_second : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| ≤ n → nth_opt …  n (l1 @ l2) = nth_opt … (n - |l1|) l2.
    142 #A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/
    143 qed.
    144136
    145137lemma frame_sem_exp_cons : ∀env.∀e.∀n1,n2.
Note: See TracChangeset for help on using the changeset viewer.