Ignore:
Timestamp:
Nov 23, 2010, 4:43:34 PM (10 years ago)
Author:
sacerdot
Message:
  • use standard notation for exponential
  • Bit is now Bool
File:
1 edited

Legend:

Unmodified
Added
Removed

  • 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.