equal
deleted
inserted
replaced
706 end*} |
706 end*} |
707 |
707 |
708 text {* |
708 text {* |
709 The value @{ML_ind empty in Vartab} stands for the empty type environment, |
709 The value @{ML_ind empty in Vartab} stands for the empty type environment, |
710 which is the value for starting the unification without any |
710 which is the value for starting the unification without any |
711 instantiations.\footnote{\bf FIXME: what is 0?} |
711 instantiations.\footnote{\bf FIXME: what is 0?} In case of a failure |
|
712 @{ML typ_unify in Sign} will throw the exception @{ML_text TUNIFY}. |
712 We can print out the resulting type environment @{ML tyenv_unif} |
713 We can print out the resulting type environment @{ML tyenv_unif} |
713 with the built-in function @{ML_ind dest in Vartab}. |
714 with the built-in function @{ML_ind dest in Vartab}. |
714 |
715 |
715 @{ML_response_fake [display,gray] |
716 @{ML_response_fake [display,gray] |
716 "Vartab.dest tyenv_unif" |
717 "Vartab.dest tyenv_unif" |
769 in |
770 in |
770 Sign.typ_match @{theory} (pat, ty) Vartab.empty |
771 Sign.typ_match @{theory} (pat, ty) Vartab.empty |
771 end*} |
772 end*} |
772 |
773 |
773 text {* |
774 text {* |
774 Printing out the calculated matcher gives |
775 In case of failure, @{ML typ_match in Sign} will throw the exception |
|
776 @{ML_text TYPE_MATCH}. Printing out the calculated matcher gives |
775 |
777 |
776 @{ML_response_fake [display,gray] |
778 @{ML_response_fake [display,gray] |
777 "pretty_tyenv @{context} tyenv_match" |
779 "pretty_tyenv @{context} tyenv_match" |
778 "[?'a := bool list, ?'b := nat]"} |
780 "[?'a := bool list, ?'b := nat]"} |
779 |
781 |