Changeset 1463 for src/utilities/adt


Ignore:
Timestamp:
Oct 25, 2011, 5:33:53 PM (9 years ago)
Author:
mulligan
Message:

added erasure for lin

File:
1 edited

Legend:

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

    r1223 r1463  
    55
    66axiom set: Type[0] → Type[0].
     7
     8inductive set (elt_type: Type[0]): Type[0] ≝
     9  | empty: set elt_type
     10  | node : nat → set elt_type → elt_type → set elt_type → set elt_type.
     11
    712axiom set_empty: ∀elt_type. set elt_type.
    813
Note: See TracChangeset for help on using the changeset viewer.