equal
deleted
inserted
replaced
999 \begin{readmore} |
999 \begin{readmore} |
1000 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1000 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see |
1001 the file @{ML_file "Pure/thm.ML"}. |
1001 the file @{ML_file "Pure/thm.ML"}. |
1002 \end{readmore} |
1002 \end{readmore} |
1003 |
1003 |
1004 \begin{exercise} |
|
1005 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
|
1006 result that type-checks. |
|
1007 \end{exercise} |
|
1008 |
|
1009 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
1004 Remember Isabelle follows the Church-style typing for terms, i.e., a term contains |
1010 enough typing information (constants, free variables and abstractions all have typing |
1005 enough typing information (constants, free variables and abstractions all have typing |
1011 information) so that it is always clear what the type of a term is. |
1006 information) so that it is always clear what the type of a term is. |
1012 Given a well-typed term, the function @{ML type_of} returns the |
1007 Given a well-typed term, the function @{ML type_of} returns the |
1013 type of a term. Consider for example: |
1008 type of a term. Consider for example: |
1035 |
1030 |
1036 @{ML_response [display,gray] |
1031 @{ML_response [display,gray] |
1037 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"} |
1032 "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"} |
1038 |
1033 |
1039 where no error is detected. |
1034 where no error is detected. |
|
1035 |
|
1036 \begin{exercise}\label{fun:revsum typed} |
|
1037 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
|
1038 result that type-checks. |
|
1039 \end{exercise} |
1040 |
1040 |
1041 Sometimes it is a bit inconvenient to construct a term with |
1041 Sometimes it is a bit inconvenient to construct a term with |
1042 complete typing annotations, especially in cases where the typing |
1042 complete typing annotations, especially in cases where the typing |
1043 information is redundant. A short-cut is to use the ``place-holder'' |
1043 information is redundant. A short-cut is to use the ``place-holder'' |
1044 type @{ML "dummyT"} and then let type-inference figure out the |
1044 type @{ML "dummyT"} and then let type-inference figure out the |