Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Integers.ma

    r1512 r1516  
    124124
    125125lemma eq_dec: ∀x,y: int. (x = y) + (x ≠ y).
    126 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?) #E
     126#x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → ?); #E
    127127[ %1 lapply E @(eq_bv_elim … x y) [ // | #_ #X destruct ]
    128128| %2 lapply E @(eq_bv_elim … x y) [ #_ #X destruct | /2/ ]
Note: See TracChangeset for help on using the changeset viewer.