Changeset 783 for src/RTL/RTL.ma


Ignore:
Timestamp:
Apr 29, 2011, 1:36:35 PM (10 years ago)
Author:
mulligan
Message:

rtl to ertl pass complete (modulo some straightforward axioms that need filling in) and refactoring to get rid of all the option types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r782 r783  
    6161  rtl_pr_main: option ident
    6262}.
     63
     64definition rtl_pr_vars: rtl_program → list (ident × nat).
     65  # P
     66  cases P
     67  # H1 # H2 # H3
     68  @ H1
     69qed.
Note: See TracChangeset for help on using the changeset viewer.