Next: Constraints on Type Declarations, Previous: Default Arguments for Code, Up: Type Declarations [Contents]


Doc Strings

Again, we borrow the idea of doc strings from Python where triple quoted strings can accompany definitions. For us we use single quoted strings that immediately follow a type declaration as below (and in the examples above).
dyn age_of(H:human,A:age)
"H is a human, A is an age"

fun fact(N:nat) -> nat
"Returns the factorial of N"

def man ::= roger | tom | bill | alan | graham | keith |
sam | fred
"The allowed men in the application"

It is quite common in doc strings to refer to the arguments. We support this by allowing the type declaration to be preceeded by a variable with that variable being used in the doc string (as in the examples above). This is purely to aid doc strings and has no semantic implications for the declarations.

In a similar way that doc string in Python are shown when the user uses help we use types for displaying user declarations or stypes for displaying system declarations.


On This Site