Ignore:
Timestamp:
Nov 23, 2010, 11:43:14 AM (9 years ago)
Author:
mulligan
Message:

Added exponential functions for nats. Working on operational semantics of processor.

File:
1 edited

Legend:

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

    r248 r257  
    5555ndefinition zero ≝
    5656  λn: Nat.
    57     replicate Bool n False.
     57    ((replicate Bool n False): BitVector n).
    5858   
    5959ndefinition max ≝
    6060  λn: Nat.
    61     replicate Bool n True.
     61    ((replicate Bool n True): BitVector n).
    6262   
    6363ndefinition append ≝
Note: See TracChangeset for help on using the changeset viewer.