Ignore:
Timestamp:
Nov 23, 2010, 4:39:31 PM (9 years ago)
Author:
sacerdot
Message:
  • new notation ...? for vectors to reduce ambiguity
  • preinstruction type ported to Matita
File:
1 edited

Legend:

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

    r261 r262  
    2626(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2727
    28 interpretation "Vector nil" 'nil = (Empty ?).
     28notation "[[ list0 x sep ; ]]"
     29  non associative with precedence 90
     30  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
     31
     32interpretation "Vector vnil" 'vnil = (Empty ?).
     33interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
    2934interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).
    30 
    31 notation "hvbox (v break !! n)"
    32   non associative with precedence 90
    33   for @{ 'get_index $v $n }.
    3435
    3536(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    8182   
    8283interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
    83    
     84
     85(*
    8486nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
    8587  (match m with
     
    98100    nassumption.
    99101nqed.
     102*)
    100103   
    101104nlet rec set_index_weak (A: Type[0]) (n: Nat)
     
    224227    ].
    225228   
    226 notation "v break @ q"
    227   right associative with precedence 47
    228   for @{ 'append $v $q }.
    229  
    230229interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
    231230   
Note: See TracChangeset for help on using the changeset viewer.