@@ -1563,10 +1563,10 @@ to:
15631563\begin{SaveVerbatim}{showdata}
15641564
15651565data Show : Type -> Type where
1566− instanceShow : (show : a -> String) -> Show a
1566+ InstanceShow : (show : a -> String) -> Show a
15671567
15681568show : Show a -> a -> String
1569−show (instanceShow show') = show'
1569+show (InstanceShow show') = show'
15701570
15711571\end{SaveVerbatim}
15721572\useverb{showdata}
@@ -1577,7 +1577,7 @@ An instance for a type \texttt{a} is then a value of type \texttt{Show a}; for e
15771577\begin{SaveVerbatim}{shownatf}
15781578
15791579showNat : Show Nat
1580−showNat = instanceShow show' where
1580+showNat = InstanceShow show' where
15811581 show' : Nat -> String
15821582 show' O = "O"
15831583 show' (S k) = "s" ++ show k
@@ -1593,7 +1593,7 @@ the function declaration for the instance. For example, for \texttt{Show (List a
15931593\begin{SaveVerbatim}{showlista}
15941594
15951595showList : Show a => Show (List a)
1596−showList = instanceShow show' where
1596+showList = InstanceShow show' where
15971597 show' : List a -> String
15981598 show' [] = "[]"
15991599 show' (x :: xs) = show x ++ " :: " ++ show xs
@@ -1622,17 +1622,17 @@ This translates to:
16221622\begin{SaveVerbatim}{orddata}
16231623
16241624data Ord : Type -> Type where
1625− instanceOrd : Eq a => (compare : a -> a -> Ordering) ->
1625+ InstanceOrd : Eq a => (compare : a -> a -> Ordering) ->
16261626 (max : a -> a -> a) -> Ord a
16271627
16281628\end{SaveVerbatim}
16291629
16301630\begin{SaveVerbatim}{orddatab}
16311631compare : Ord a -> a -> a -> Ordering
1632−compare (instanceOrd compare' max') = compare'
1632+compare (InstanceOrd compare' max') = compare'
16331633
1634−max : Ord a -> a -> a -> Ordering
1635−max (instanceOrd compare' max') = max'
1634+max : Ord a -> a -> a -> a
1635+max (InstanceOrd compare' max') = max'
16361636
16371637\end{SaveVerbatim}
16381638\useverb{orddata}
@@ -1646,7 +1646,7 @@ dictionary, to assist with class resolution. In this case:
16461646\begin{SaveVerbatim}{ordparent}
16471647
16481648OrdEq : Ord a -> Eq a
1649−OrdEq (instanceOrd {{eq}} compare' max') = eq
1649+OrdEq (InstanceOrd {{eq}} compare' max') = eq
16501650
16511651\end{SaveVerbatim}
16521652\useverb{ordparent}
@@ -1686,7 +1686,9 @@ In general, \texttt{class} declarations are elaborated as follows:
16861686Then \texttt{instance} declarations are elaborated as follows. One complication
16871687is that the function definitions in an \texttt{instance} declaration do not
16881688have 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
1691+defined instance:
16901692
16911693\DM{
16921694\AR{
@@ -1757,19 +1759,20 @@ max x y = if (x > y) then x else y
17571759
17581760If $\MO{Trivial}$ does not find a solution, $\MO{Instance}$ begins a global search,
17591761applying 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+of type $\ttt$:
17611764
17621765\DM{
1763−\MO{TryInstance}\;(\FN{instanceC}\;\ta)\;\mq\;\RW{do}\;
1766+\MO{TryInstance}\;\FN{instanceC}\;\mq\;\RW{do}\;
17641767\AR{
1765−\vec{\MO{Claim}}\;(\tx\Hab\ta)\\
1768+\vec{\MO{Claim}}\;(\tx\Hab\ttt)\\
17661769\ttinterp{\FN{instanceC};\tx}\\
17671770\vec{\MO{Focus}}\;\tx;\;\vec{\MO{Instance}}
17681771}
17691772}
17701773
17711774We 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:
17731776
17741777\DM{
17751778\MO{Instance}\;\mq\;