git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3753 from justjoheinz/docs/fix_refl

Fix references to refl in misc reference

commitbccb3a5ca2d6e1331a2550fa4463205486245d54 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateFri 14 Apr 2017, 12:59 (10 years ago) parent4bbe9c52d02b09
2 files changed+6−6
compare with master
unifiedsplit
docs/reference/misc.rst+3−3 docs/tutorial/syntax.rst+3−3
docs/reference/misc.rst+3−3
@@ -51,7 +51,7 @@ some constructors of proofs.
5151
5252::
5353
54− syntax Trivial = (| oh, refl |)
54+ syntax Trivial = (| Oh, Refl |)
5555
5656
5757Totality checking assertions
@@ -296,13 +296,13 @@ can be used in proofs, for example:
296296 -- Base case
297297 (Z + m = m + Z) <== plus_comm =
298298 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
299− (Z + m = m) in refl
299+ (Z + m = m) in Refl
300300
301301 -- Step case
302302 (S k + m = m + S k) <== plus_comm =
303303 rewrite ((k + m = m + k) <== plus_comm) in
304304 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
305− refl
305+ Refl
306306
307307Reflection
308308==========
docs/tutorial/syntax.rst+3−3
@@ -74,14 +74,14 @@ bound is below the upper bound using ``so``:
7474
7575 data Interval : Type where
7676 MkInterval : (lower : Double) -> (upper : Double) ->
77− so (lower < upper) -> Interval
77+ So (lower < upper) -> Interval
7878
79−We can define a syntax which, in patterns, always matches ``oh`` for
79+We can define a syntax which, in patterns, always matches ``Oh`` for
8080the proof argument, and in terms requires a proof term to be provided:
8181
8282.. code-block:: idris
8383
84− pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
84+ pattern syntax "[" [x] "..." [y] "]" = MkInterval x y Oh
8585 term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
8686
8787In terms, the syntax ``[x...y]`` will generate a proof obligation