git.iko.soy/Idris-dev
on master help sign in
Fix implication that implicit relates to totality
4b667a9Jason Felice
docs/reference/syntax-guide.rst+7−1
compare with master
unifiedsplit
@@ -387,10 +387,16 @@ Totality
387::
387::
388
388
389 total
389 total
390− implicit
391 partial
390 partial
392 covering
391 covering
393
392
393+Implicit Coercion
394+^^^^^^^^^^^^^^^^^
395+
396+::
397+
398+ implicit
399+
394Options
400Options
395^^^^^^^
401^^^^^^^
396
402