on master help sign in
remove some duplicated definitions and tidy up
commit540e76bb8917f42634dedba564436ac7aaf0862e authorMartin Baker <git87465@martinb.com> dateSat 18 May 2019, 11:39 (7 years ago) parent654c431
1 file changed+5−23
docs/proofs/primitive.rst+5−23
docs/proofs/primitive.rst+5−23
@@ -1,7 +1,7 @@
11Primitive Operators
22===================
33
4−.. list-table:: Primitive Operators
4+.. list-table::
55 :widths: 10 30
66 :stub-columns: 1
77
@@ -329,7 +329,7 @@ Primitive Operators
329329Read and Write State
330330====================
331331
332−.. list-table:: Read and Write State
332+.. list-table::
333333 :widths: 10 30
334334 :stub-columns: 1
335335
@@ -375,13 +375,6 @@ Read and Write State
375375
376376 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
377377
378− .. code-block:: idris
379−
380− lookupTyExact n = case !(lookupTy n) of
381− [res] => pure res
382− [] => fail [NamePart n, TextPart "is not defined."]
383− xs => fail [NamePart n, TextPart "is ambiguous."]
384−
385378 * - lookupDatatype
386379 - Find the reflected representation of all datatypes whose names are overloadings of some name.
387380
@@ -396,15 +389,6 @@ Read and Write State
396389
397390 lookupDatatypeExact : TTName -> Elab Datatype
398391
399− .. code-block:: idris
400−
401− lookupDatatypeExact n = case !(lookupDatatype n) of
402− [res] => pure res
403− [] => fail [TextPart
404− "No datatype named", NamePart n]
405− xs => fail [TextPart "More than one datatype named",
406− NamePart n]
407−
408392 * - lookupFunDefn
409393 - Find the reflected function definition of all functions whose names are overloadings of some name.
410394
@@ -427,14 +411,12 @@ Read and Write State
427411 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
428412
429413 * - lookupArgsExact
430− - Get the argument specification for a name. Fail if the name does not uniquely resolve.
414+ - Get the argument specification for a name. Fail if the name does not uniquely resolve.
431415
432416 Signature:
433417
434418 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
435419
436− .. code-block:: idris
437−
438420 * - check
439421 - Attempt to type-check a term, getting back itself and its type.
440422
@@ -448,7 +430,7 @@ Read and Write State
448430Error Handling
449431==============
450432
451−.. list-table:: Error Handling
433+.. list-table::
452434 :widths: 10 30
453435 :stub-columns: 1
454436
@@ -460,7 +442,7 @@ Error Handling
460442
461443 tryCatch : Elab a -> (Err -> Elab a) -> Elab a
462444
463− Fixme - following does not work.
445+ Fixme - following does not work.
464446
465447 .. code-block:: idris
466448