equal
deleted
inserted
replaced
317 section {*** lets with single assignments ***} |
317 section {*** lets with single assignments ***} |
318 |
318 |
319 datatype rtrm2 = |
319 datatype rtrm2 = |
320 rVr2 "name" |
320 rVr2 "name" |
321 | rAp2 "rtrm2" "rtrm2" |
321 | rAp2 "rtrm2" "rtrm2" |
322 | rLm2 "name" "rtrm2" |
322 | rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)" |
323 | rLt2 "rassign" "rtrm2" |
323 | rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)" |
324 and rassign = |
324 and rassign = |
325 rAs "name" "rtrm2" |
325 rAs "name" "rtrm2" |
326 |
326 |
327 (* to be given by the user *) |
327 (* to be given by the user *) |
328 primrec |
328 primrec |
409 section {*** lets with many assignments ***} |
409 section {*** lets with many assignments ***} |
410 |
410 |
411 datatype trm3 = |
411 datatype trm3 = |
412 Vr3 "name" |
412 Vr3 "name" |
413 | Ap3 "trm3" "trm3" |
413 | Ap3 "trm3" "trm3" |
414 | Lm3 "name" "trm3" |
414 | Lm3 "name" "trm3" --"bind (name) in (trm3)" |
415 | Lt3 "assigns" "trm3" |
415 | Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)" |
416 and assigns = |
416 and assigns = |
417 ANil |
417 ANil |
418 | ACons "name" "trm3" "assigns" |
418 | ACons "name" "trm3" "assigns" |
419 |
419 |
420 (* to be given by the user *) |
420 (* to be given by the user *) |
504 section {*** lam with indirect list recursion ***} |
504 section {*** lam with indirect list recursion ***} |
505 |
505 |
506 datatype trm4 = |
506 datatype trm4 = |
507 Vr4 "name" |
507 Vr4 "name" |
508 | Ap4 "trm4" "trm4 list" |
508 | Ap4 "trm4" "trm4 list" |
509 | Lm4 "name" "trm4" |
509 | Lm4 "name" "trm4" --"bind (name) in (trm)" |
510 |
510 |
511 thm trm4.recs |
511 thm trm4.recs |
512 |
512 |
513 primrec |
513 primrec |
514 fv_trm4 and fv_trm4_list |
514 fv_trm4 and fv_trm4_list |
594 |
594 |
595 |
595 |
596 datatype rtrm5 = |
596 datatype rtrm5 = |
597 rVr5 "name" |
597 rVr5 "name" |
598 | rAp5 "rtrm5" "rtrm5" |
598 | rAp5 "rtrm5" "rtrm5" |
599 | rLt5 "rlts" "rtrm5" |
599 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" |
600 and rlts = |
600 and rlts = |
601 rLnil |
601 rLnil |
602 | rLcons "name" "rtrm5" "rlts" |
602 | rLcons "name" "rtrm5" "rlts" |
603 |
603 |
604 primrec |
604 primrec |