Small text/example fix

Zalastax · Apr 4, 2018 · f11d1a9 · f11d1a9
1 parent 6739fbb
commit f11d1a9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 5 deletions.
diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex
@@ -375,14 +375,13 @@
 Agda implements a sort of subtyping for sizes,
 so computations of different sizes can still be composed via bind.
 
-We don't give the constructors \AgdaRef[ActorMonad]{Return} and \AgdaRef[ActorMonad]{_∞>>=_}
+We don't give the constructors \AgdaRef[ActorMonad]{Return} and \AgdaInductiveConstructor{∞>>=}
 the names return and >>=,
 since we want those names to refer to the type \AgdaRef[ActorMonad]{∞ActorM}.
 Instead, the actual return and >>= are defined as a separate functions
-that wrap \AgdaRef[ActorMonad]{Return} and \AgdaRef[ActorMonad]{_∞>>=_}.
+that wrap \AgdaRef[ActorMonad]{Return} and \AgdaInductiveConstructor{∞>>=}.
 
 \AgdaTarget{Return}
-\AgdaTarget{_∞>>=_}
 \begin{code}
   Return : ∀ {A post} → (val : A) → ActorM i IS A (post val) post
   _∞>>=_ : ∀ {A B pre mid post} → (m : ∞ActorM i IS A pre mid) →

diff --git a/src/Examples/Types.lagda.tex b/src/Examples/Types.lagda.tex
@@ -16,8 +16,10 @@
 data _≡_ {a} {A : Set a} (x : A) : A → Set a where
   refl : x ≡ x
 
-trivial = 4 ≡ 4
-definitional = (2 + 2) ≡ 4
+trivial : 4 ≡ 4
+trivial = refl
+definitional : (2 + 2) ≡ 4
+definitional = refl
 \end{code}
 %</PropositionalEquality>