Changeset 263


Ignore:
Timestamp:
Nov 23, 2010, 4:43:34 PM (9 years ago)
Author:
sacerdot
Message:
  • use standard notation for exponential
  • Bit is now Bool
Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r262 r263  
    1818
    1919ndefinition BitVector ≝ λn: Nat. Vector Bool n.
    20 ndefinition Bit ≝ BitVector (S Z).
     20ndefinition Bit ≝ Bool.
    2121ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
    2222ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
  • Deliverables/D4.1/Matita/Exponential.ma

    r257 r263  
    77include "Equality.ma".
    88include "Connectives.ma".
    9 
    10 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    11 (* Syntax.                                                                    *)
    12 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    13 
    14 notation "hvbox(n^m)"
    15   left associative with precedence 52
    16   for @{ 'exponential $n $m }.
    179
    1810(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.