Changeset 715


Ignore:
Timestamp:
Mar 29, 2011, 1:49:57 PM (9 years ago)
Author:
mulligan
Message:

Restored rev from Util as it appears that list reversal is not a part of the standard library, but a local modification.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r712 r715  
    2323  | false ⇒ f
    2424  ].
     25
     26let rec rev (A: Type[0]) (l: list A) on l ≝
     27  match l with
     28  [ nil ⇒ nil A
     29  | cons hd tl ⇒ (rev A tl) @ [ hd ]
     30  ].
    2531   
    2632(*
  • src/LTL/LTLToLIN.ma

    r714 r715  
    1717    | LTL_St_Pop lbl ⇒ LIN_St_Pop globals
    1818    | LTL_St_Push lbl ⇒ LIN_St_Push globals
    19     | LTL_St_Address ident proof address lbl ⇒ LIN_St_Address globals ident proof
    20     | _ ⇒ ?
     19(*    | LTL_St_Address ident proof address lbl ⇒ LIN_St_Address globals ident proof *)
     20    | LTL_St_FromAcc
    2121    ].
Note: See TracChangeset for help on using the changeset viewer.