Changeset 3466 for src/ASM


Ignore:
Timestamp:
Mar 7, 2014, 12:52:28 PM (6 years ago)
Author:
asperti
Message:

Removed function that is only in the standard library.
Maaaany more to be removed.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Util.ma

    r2700 r3466  
    633633qed.
    634634
    635 lemma append_nil:
    636   ∀A: Type[0].
    637   ∀l: list A.
    638     l @ [ ] = l.
    639   #A #L
    640   elim L //
    641 qed.
    642 
    643635lemma rev_append:
    644636  ∀A: Type[0].
Note: See TracChangeset for help on using the changeset viewer.