Changeset 1296 for src/utilities


Ignore:
Timestamp:
Oct 5, 2011, 5:53:54 PM (8 years ago)
Author:
mulligan
Message:

changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/adt/table_adt.ma

    r1285 r1296  
    112112        match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
    113113        [ empty ⇒ λabsurd. ?
    114         | node _ lrv lrd lrl lrr ⇒ λ
     114        | node _ lrv lrd lrl lrr ⇒ λnon_empty_proof.
    115115            tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right)
    116         ]
     116        ] ?
    117117    ] left_proof
    118118  | false ⇒ ?
    119119  ].
    120120  [1: normalize in absurd;
     121      elim absurd
     122      #ABSURD
     123      @⊥ @ABSURD @I
     124  |3: normalize in absurd;
    121125      elim absurd
    122126      #ABSURD
Note: See TracChangeset for help on using the changeset viewer.