@@ -1563,10 +1563,10 @@ to:
1563\begin{SaveVerbatim}{showdata}
1563\begin{SaveVerbatim}{showdata}
1565data Show : Type -> Type where
1565data Show : Type -> Type where
1566− instanceShow : (show : a -> String) -> Show a
1566+ InstanceShow : (show : a -> String) -> Show a
1568show : Show a -> a -> String
1568show : Show a -> a -> String
1569−show (instanceShow show') = show'
1569+show (InstanceShow show') = show'
1571\end{SaveVerbatim}
1571\end{SaveVerbatim}
1572\useverb{showdata}
1572\useverb{showdata}
@@ -1577,7 +1577,7 @@ An instance for a type \texttt{a} is then a value of type \texttt{Show a}; for e
1577\begin{SaveVerbatim}{shownatf}
1577\begin{SaveVerbatim}{shownatf}
1579showNat : Show Nat
1579showNat : Show Nat
1580−showNat = instanceShow show' where
1580+showNat = InstanceShow show' where
1581 show' : Nat -> String
1581 show' : Nat -> String
1582 show' O = "O"
1582 show' O = "O"
1583 show' (S k) = "s" ++ show k
1583 show' (S k) = "s" ++ show k
@@ -1593,7 +1593,7 @@ the function declaration for the instance. For example, for \texttt{Show (List a
1593\begin{SaveVerbatim}{showlista}
1593\begin{SaveVerbatim}{showlista}
1595showList : Show a => Show (List a)
1595showList : Show a => Show (List a)
1596−showList = instanceShow show' where
1596+showList = InstanceShow show' where
1597 show' : List a -> String
1597 show' : List a -> String
1598 show' [] = "[]"
1598 show' [] = "[]"
1599 show' (x :: xs) = show x ++ " :: " ++ show xs
1599 show' (x :: xs) = show x ++ " :: " ++ show xs
@@ -1622,17 +1622,17 @@ This translates to:
1622\begin{SaveVerbatim}{orddata}
1622\begin{SaveVerbatim}{orddata}
1624data Ord : Type -> Type where
1624data Ord : Type -> Type where
1625− instanceOrd : Eq a => (compare : a -> a -> Ordering) ->
1625+ InstanceOrd : Eq a => (compare : a -> a -> Ordering) ->
1626 (max : a -> a -> a) -> Ord a
1626 (max : a -> a -> a) -> Ord a
1628\end{SaveVerbatim}
1628\end{SaveVerbatim}
1630\begin{SaveVerbatim}{orddatab}
1630\begin{SaveVerbatim}{orddatab}
1631compare : Ord a -> a -> a -> Ordering
1631compare : Ord a -> a -> a -> Ordering
1632−compare (instanceOrd compare' max') = compare'
1632+compare (InstanceOrd compare' max') = compare'
1634−max : Ord a -> a -> a -> Ordering
1634+max : Ord a -> a -> a -> a
1635−max (instanceOrd compare' max') = max'
1635+max (InstanceOrd compare' max') = max'
1637\end{SaveVerbatim}
1637\end{SaveVerbatim}
1638\useverb{orddata}
1638\useverb{orddata}
@@ -1646,7 +1646,7 @@ dictionary, to assist with class resolution. In this case:
1646\begin{SaveVerbatim}{ordparent}
1646\begin{SaveVerbatim}{ordparent}
1648OrdEq : Ord a -> Eq a
1648OrdEq : Ord a -> Eq a
1649−OrdEq (instanceOrd {{eq}} compare' max') = eq
1649+OrdEq (InstanceOrd {{eq}} compare' max') = eq
1651\end{SaveVerbatim}
1651\end{SaveVerbatim}
1652\useverb{ordparent}
1652\useverb{ordparent}
@@ -1686,7 +1686,9 @@ In general, \texttt{class} declarations are elaborated as follows:
1686Then \texttt{instance} declarations are elaborated as follows. One complication
1686Then \texttt{instance} declarations are elaborated as follows. One complication
1687is that the function definitions in an \texttt{instance} declaration do not
1687is that the function definitions in an \texttt{instance} declaration do not
1688have explicit types, so we must retrieve the method types from the system state
1688have explicit types, so we must retrieve the method types from the system state
1689−and substitute $\TC{C}\;\ttt$, using $\MO{ExpandTypes}$:
1689+and substitute $\TC{C}\;\ttt$, using $\MO{ExpandTypes}$.
1690+The name $\FN{instanceC}$ is a fresh name generated for the newly
@@ -1757,19 +1759,20 @@ max x y = if (x > y) then x else y
1758If $\MO{Trivial}$ does not find a solution, $\MO{Instance}$ begins a global search,
1760If $\MO{Trivial}$ does not find a solution, $\MO{Instance}$ begins a global search,
1759applying every class instance, and attempting to resolve the instance's parameters
1761applying every class instance, and attempting to resolve the instance's parameters
1760−recursively. Given an instance $\FN{instanceC}$ with parameters $\ta$:
1762+recursively. Given an instance function $\FN{instanceC}$ with parameters
1763−\MO{TryInstance}\;(\FN{instanceC}\;\ta)\;\mq\;\RW{do}\;
1766+\MO{TryInstance}\;\FN{instanceC}\;\mq\;\RW{do}\;
1765−\vec{\MO{Claim}}\;(\tx\Hab\ta)\\
1768+\vec{\MO{Claim}}\;(\tx\Hab\ttt)\\
1766\ttinterp{\FN{instanceC};\tx}\\
1769\ttinterp{\FN{instanceC};\tx}\\
1767\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}
1770\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}
1771We define $\MO{Instance}$ as follows, using $\MO{AllInstances}$ to retrieve
1774We define $\MO{Instance}$ as follows, using $\MO{AllInstances}$ to retrieve
1772−all possible instances in the form required by $\MO{TryInstance}$:
1775+all functions which define instances:
1775\MO{Instance}\;\mq\;
1778\MO{Instance}\;\mq\;