git.iko.soy/Idris-dev
on master help sign in
Fix reference to "refl" in misc reference
2d02b09Markus Klink
docs/reference/misc.rst+3−3
compare with master
unifiedsplit
@@ -51,7 +51,7 @@ some constructors of proofs.
51
51
52::
52::
53
53
54− syntax Trivial = (| oh, refl |)
54+ syntax Trivial = (| Oh, Refl |)
55
55
56
56
57Totality checking assertions
57Totality checking assertions
@@ -296,13 +296,13 @@ can be used in proofs, for example:
296 -- Base case
296 -- Base case
297 (Z + m = m + Z) <== plus_comm =
297 (Z + m = m + Z) <== plus_comm =
298 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
298 rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
299− (Z + m = m) in refl
299+ (Z + m = m) in Refl
300
300
301 -- Step case
301 -- Step case
302 (S k + m = m + S k) <== plus_comm =
302 (S k + m = m + S k) <== plus_comm =
303 rewrite ((k + m = m + k) <== plus_comm) in
303 rewrite ((k + m = m + k) <== plus_comm) in
304 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
304 rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
305− refl
305+ Refl
306
306
307Reflection
307Reflection
308==========
308==========
docs/tutorial/syntax.rst+3−3
@@ -74,14 +74,14 @@ bound is below the upper bound using ``so``:
74
74
75 data Interval : Type where
75 data Interval : Type where
76 MkInterval : (lower : Double) -> (upper : Double) ->
76 MkInterval : (lower : Double) -> (upper : Double) ->
77− so (lower < upper) -> Interval
77+ So (lower < upper) -> Interval
78
78
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
80the proof argument, and in terms requires a proof term to be provided:
80the proof argument, and in terms requires a proof term to be provided:
81
81
82.. code-block:: idris
82.. code-block:: idris
83
83
84− pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
84+ pattern syntax "[" [x] "..." [y] "]" = MkInterval x y Oh
85 term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
85 term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
86
86
87In terms, the syntax ``[x...y]`` will generate a proof obligation
87In terms, the syntax ``[x...y]`` will generate a proof obligation