Changeset 2476 for src/common


Ignore:
Timestamp:
Nov 19, 2012, 6:04:24 PM (7 years ago)
Author:
piccolo
Message:

fixed commutation lemmas in lineariseProof
started proof of main theorem in lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/extraGlobalenvs.ma

    r2474 r2476  
    193193  Σi.is_internal_function_of_program ?? prog i ≝
    194194  λA,B,init,prog,f.«f, is_internal_function_of_program_ok … (pi2 … f)».
    195 
    196 coercion if_in_prog_from_if_in_global_env nocomposites :
    197   ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.
    198   ∀f:Σi.is_internal_function ? (globalenv ?? init prog) i.
    199   Σi.is_internal_function_of_program ?? prog i ≝
    200   if_in_global_env_to_if_in_prog
    201   on _f : Sig ident (λi.is_internal_function ?? i)
    202   to Sig ident (λi.is_internal_function_of_program ??? i).
    203195
    204196lemma if_propagate :
Note: See TracChangeset for help on using the changeset viewer.