ProgTutorial/Solutions.thy
changeset 426 d94755882e36
parent 424 5e0a2b50707e
child 440 a0b280dd4bc7
equal deleted inserted replaced
425:ce43c04d227d 426:d94755882e36
    88    Number of int
    88    Number of int
    89  | Mult of expr * expr 
    89  | Mult of expr * expr 
    90  | Add of expr * expr
    90  | Add of expr * expr
    91 
    91 
    92 fun parse_basic xs =
    92 fun parse_basic xs =
    93   (OuterParse.nat >> Number 
    93   (Parse.nat >> Number 
    94    || OuterParse.$$$ "(" |-- parse_expr --| OuterParse.$$$ ")") xs
    94    || Parse.$$$ "(" |-- parse_expr --| Parse.$$$ ")") xs
    95 and parse_factor xs =
    95 and parse_factor xs =
    96   (parse_basic --| OuterParse.$$$ "*" -- parse_factor >> Mult 
    96   (parse_basic --| Parse.$$$ "*" -- parse_factor >> Mult 
    97    || parse_basic) xs
    97    || parse_basic) xs
    98 and parse_expr xs =
    98 and parse_expr xs =
    99   (parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add 
    99   (parse_factor --| Parse.$$$ "+" -- parse_expr >> Add 
   100    || parse_factor) xs*}
   100    || parse_factor) xs*}
   101 
   101 
   102 
   102 
   103 text {* \solution{ex:dyckhoff} *}
   103 text {* \solution{ex:dyckhoff} *}
   104 
   104