Changeset 1884 for src/Cminor


Ignore:
Timestamp:
Apr 9, 2012, 3:07:06 PM (8 years ago)
Author:
campbell
Message:

Syntax changes to fit Paolo's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1878 r1884  
    431431
    432432lemma choose_regs_length : ∀le,env,es,f,p,f',rs.
    433   choose_regs le env es f p = ❬f',rs❭ → |es| = |rs|.
     433  choose_regs le env es f p = ❬f',rs❭ → |es| = length … rs.
    434434#le #env #es #f #p #f' * #rs #H #_ @sym_eq @(All2_length … H)
    435435qed.
     
    571571
    572572let rec add_exprs (le:label_env) (env:env) (es:list (𝚺t:typ.expr t)) (Env:All ? (exprtyp_present env) es)
    573                   (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le env)
     573                  (dsts:list register) (pf:length … es = length … dsts) (f:partial_fn le env)
    574574                  (Hdsts:All2 ?? (λr,e. fn_env_has le env f r (eject' typ expr e)) dsts es) on es: Σf':partial_fn le env. fn_contains le env f f' ≝
    575575match es return λes.All ?? es → All2 ???? es → |es|=|dsts| → ? with
Note: See TracChangeset for help on using the changeset viewer.