Changeset 247


Ignore:
Timestamp:
Nov 22, 2010, 11:12:56 AM (9 years ago)
Author:
mulligan
Message:

Changes to get directory to compile.

Location:
Deliverables/D4.1/Matita
Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Either.ma

    r228 r247  
    22include "Maybe.ma".
    33
    4 include "logic/pts.ma".
     4include "Universes.ma".
    55
    66ninductive Either (A: Type[0]) (B: Type[0]): Type[0] ≝
  • Deliverables/D4.1/Matita/List.ma

    r242 r247  
    44
    55include "Util.ma".
    6 
    7 include "logic/pts.ma".
    8 
     6include "Universes.ma".
    97include "Nat.ma".
    10 
    11 include "Maybe.ma".
    12 
    13 include "Plogic/equality.ma".
     8(* include "Maybe.ma". *)
     9include "Equality.ma".
    1410
    1511(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Maybe.ma

    r228 r247  
    11include "Bool.ma".
    22
    3 include "logic/pts.ma".
    4 include "Plogic/equality.ma".
     3include "Universes.ma".
     4include "Equality.ma".
    55
    66ninductive Maybe (A: Type[0]): Type[0] ≝
  • Deliverables/D4.1/Matita/Nat.ma

    r246 r247  
    311311  //.
    312312  #N H.
    313   //.
     313  nnormalize.
     314  nrewrite < H.
     315  @.
    314316nqed.
    315317
     
    355357  #N H.
    356358  nnormalize.
    357   //.
     359  nrewrite > H.
     360  nrewrite < (plus_associative n N ?).
     361  nrewrite > (plus_symmetrical n N).
     362  nrewrite > (plus_associative N n ?).
     363  @.
    358364nqed.
    359365
     
    374380  nnormalize.
    375381  nrewrite > H.
    376   napplyS multiplication_succ.
     382  nrewrite > (multiplication_succ ? ?).
     383  @.
    377384nqed.
    378385
     
    386393  #N H.
    387394  nnormalize.
    388   //.
     395  nrewrite > (succ_plus ? ?).
     396  nrewrite < (succ_plus_succ_zero ?).
     397  @.
    389398nqed.
    390399
     
    412421  nnormalize.
    413422  nrewrite > H.
    414   napplyS plus_associative.
     423  nrewrite < (plus_associative ? ? ?).
     424  @.
    415425nqed.
    416426
     
    419429    o * (m + n) = o * m + o * n.
    420430  #m n o.
    421   napplyS multiplication_symmetrical.
     431  nelim o.
     432  //.
     433  #N H.
     434  nnormalize.
     435  nrewrite > H.
     436  nrewrite < (plus_associative ? n (N * n)).
     437  nrewrite > (plus_symmetrical (m + N * m) n).
     438  nrewrite < (plus_associative n m (N * m)).
     439  nrewrite < (plus_symmetrical n m).
     440  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
     441  @.
    422442nqed.
    423443
     
    432452  nnormalize.
    433453  nrewrite > H.
    434   napplyS multiplication_distributes_right_plus.
     454  nrewrite > (multiplication_distributes_right_plus ? ? ?).
     455  @.
    435456nqed.
    436457
Note: See TracChangeset for help on using the changeset viewer.