Ignore:
Timestamp:
Nov 23, 2010, 5:44:42 PM (10 years ago)
Author:
sacerdot
Message:
  • notation moved to proper places
  • new function split on Vectors
File:
1 edited

Legend:

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

    r264 r268  
    22include "BitVectorTrie.ma".
    33include "String.ma".
    4 
    5 interpretation "Cartesian" 'product A B = (Cartesian A B).
    6 notation "hvbox(a break ⊎ b)"
    7  left associative with precedence 50
    8 for @{ 'disjoint_union $a $b }.
    9 interpretation "Either" 'disjoint_union A B = (Either A B).
    10 interpretation "Bool" 'or a b = (inclusive_disjunction a b).
    114
    125ninductive addressing_mode: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.