Changeset 878 for src/LIN


Ignore:
Timestamp:
Jun 3, 2011, 5:35:27 PM (8 years ago)
Author:
campbell
Message:

Removal of manually inserted record projections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r757 r878  
    2929  lin_pr_main: option ident
    3030}.
    31 
    32 definition lin_pr_vars:
    33     lin_program → list (ident × nat).
    34   # r
    35   cases r
    36   # H1 # H2 #H3
    37   @ H1
    38 qed.
    39 
    40 definition lin_pr_funcs:
    41   ∀p: lin_program.
    42     list (ident × (lin_function_definition (map ? ? (fst ? ?) (lin_pr_vars p)))).
    43   # r
    44   cases r
    45   # H1 # H2 #H3
    46   @ H2
    47 qed.
Note: See TracChangeset for help on using the changeset viewer.