Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (8 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/bindLists.ma

    r1636 r1647  
    7878   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
    7979
    80 notation > "νν ident l × n opt('with' ident EQ) 'in' f" with precedence 47 for
     80notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    8181 ${default
    8282   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
     
    8484 }.
    8585 
    86 notation > "νν ident l : ty × n opt('with' ident EQ) 'in' f" with precedence 47 for
     86notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    8787 ${default
    8888   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
     
    9090 }.
    9191 
    92 notation < "hvbox(νν \nbsp ident l : ty × n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
     92notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    9393   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    94 notation < "hvbox(νν_ n \nbsp ident l : ty × n \nbsp 'in' \nbsp break f)" with precedence 47 for
     94notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for
    9595   @{ 'unews $n (λ${ident l} : $ty.$f) }.
    9696
     
    112112 
    113113 
    114 coercion blist_from_list nocomposites :
     114coercion blist_from_list :
    115115  ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???.
    116116
     
    154154 
    155155definition BindList ≝
    156   λB,T.MakeMonad (mk_MonadDefinition
     156  λB,T.MakeMonadProps
    157157  (* the monad *)
    158158  (λX.bind_list B T X)
     
    161161  (* bind *)
    162162  (bbind B T)
    163   ???).
    164 [(* bind_bind *)
     163  ???.
     164[(* ret_bind *)
     165  #X#Y#x#f normalize @bappend_bnil
     166|(* bind_ret *)
     167 #X#m elim m normalize /2 by /
     168 #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi
     169|(* bind_bind *)
    165170 #X#Y#Z#m#f#g elim m normalize
    166171 [//
     
    169174 |(* case bnew *)
    170175  #t #l #Hi @bnew_proper //
     176  #x#y #x_eq_y destruct(x_eq_y) @Hi
    171177 ]
    172 |(* bind_ret *)
    173  #X#m elim m normalize /2 by /
    174  #t #l' #Hi @bnew_proper normalize // #s#t#eq destruct @Hi
    175 |(* ret_bind *)
    176   #X#Y#x#f normalize @bappend_bnil
    177178]
    178179qed.
     180
     181unification hint 0 ≔ B, T, X;
     182  N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M
     183(*--------------------------------------------*) ⊢
     184  bind_list B T X ≡ monad O X.
    179185
    180186include "utilities/state.ma".
     
    195201theorem bcompile_append :
    196202  ∀E, R, T, U, fresh, bl1, bl2.
    197   bcompile E R T U fresh (bl1 @ bl2) ≅
     203  (bcompile E R T U fresh (bl1 @ bl2)) ≅
    198204  (
    199205  ! l1 ← bcompile … fresh bl1 ;
Note: See TracChangeset for help on using the changeset viewer.