git.iko.soy/Idris-dev
on master help sign in
remove some duplicated definitions and tidy up
540e76bMartin Baker
docs/proofs/primitive.rst+5−23
compare with master
unifiedsplit
@@ -1,7 +1,7 @@
1Primitive Operators
1Primitive Operators
2===================
2===================
3
3
4−.. list-table:: Primitive Operators
4+.. list-table::
5 :widths: 10 30
5 :widths: 10 30
6 :stub-columns: 1
6 :stub-columns: 1
7
7
@@ -329,7 +329,7 @@ Primitive Operators
329Read and Write State
329Read and Write State
330====================
330====================
331
331
332−.. list-table:: Read and Write State
332+.. list-table::
333 :widths: 10 30
333 :widths: 10 30
334 :stub-columns: 1
334 :stub-columns: 1
335
335
@@ -375,13 +375,6 @@ Read and Write State
375
375
376 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
376 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
377
377
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−
385 * - lookupDatatype
378 * - lookupDatatype
386 - Find the reflected representation of all datatypes whose names are overloadings of some name.
379 - Find the reflected representation of all datatypes whose names are overloadings of some name.
387
380
@@ -396,15 +389,6 @@ Read and Write State
396
389
397 lookupDatatypeExact : TTName -> Elab Datatype
390 lookupDatatypeExact : TTName -> Elab Datatype
398
391
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−
408 * - lookupFunDefn
392 * - lookupFunDefn
409 - Find the reflected function definition of all functions whose names are overloadings of some name.
393 - Find the reflected function definition of all functions whose names are overloadings of some name.
410
394
@@ -427,14 +411,12 @@ Read and Write State
427 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
411 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
428
412
429 * - lookupArgsExact
413 * - 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.
431
415
432 Signature:
416 Signature:
433
417
434 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
418 lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
435
419
436− .. code-block:: idris
437−
438 * - check
420 * - check
439 - Attempt to type-check a term, getting back itself and its type.
421 - Attempt to type-check a term, getting back itself and its type.
440
422
@@ -448,7 +430,7 @@ Read and Write State
448Error Handling
430Error Handling
449==============
431==============
450
432
451−.. list-table:: Error Handling
433+.. list-table::
452 :widths: 10 30
434 :widths: 10 30
453 :stub-columns: 1
435 :stub-columns: 1
454
436
@@ -460,7 +442,7 @@ Error Handling
460
442
461 tryCatch : Elab a -> (Err -> Elab a) -> Elab a
443 tryCatch : Elab a -> (Err -> Elab a) -> Elab a
462
444
463− Fixme - following does not work.
445+ Fixme - following does not work.
464
446
465 .. code-block:: idris
447 .. code-block:: idris
466
448