Ignore:
Timestamp:
Dec 1, 2010, 11:18:05 AM (9 years ago)
Author:
mulligan
Message:

Added fold_right_i (with dependent type) to List file.

File:
1 edited

Legend:

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

    r343 r349  
    190190interpretation "Nat exponential" 'exponential n m = (exponential n m).
    191191
    192 nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝
     192nlet rec eq_n (m: Nat) (n: Nat) on m: Bool ≝
    193193  match m with
    194194    [ Z ⇒
     
    199199    | S o ⇒
    200200      match n with
    201         [ S p ⇒ decidable_equality o p
     201        [ S p ⇒ eq_n o p
    202202        | _ ⇒ false
    203203        ]
Note: See TracChangeset for help on using the changeset viewer.