git.iko.soy/Idris-dev
on master help sign in
Minor edits to the tutorial
adc85d7Edwin Brady
docs/tutorial/introduction.rst+1−1
compare with master
unifiedsplit
@@ -39,7 +39,7 @@ function, which concatenates vectors:
39This tutorial introduces Idris, a general purpose functional
39This tutorial introduces Idris, a general purpose functional
40programming language with dependent types. The goal of the Idris
40programming language with dependent types. The goal of the Idris
41project is to build a dependently typed language suitable for
41project is to build a dependently typed language suitable for
42−verifiable *systems* programming. To this end, Idris is a compiled
42+verifiable general purpose programming. To this end, Idris is a compiled
43language which aims to generate efficient executable code. It also has
43language which aims to generate efficient executable code. It also has
44a lightweight foreign function interface which allows easy interaction
44a lightweight foreign function interface which allows easy interaction
45with external ``C`` libraries.
45with external ``C`` libraries.
docs/tutorial/typesfuns.rst+3
@@ -973,6 +973,9 @@ updated):
973The syntax ``record { field = val, ... }`` generates a function which
973The syntax ``record { field = val, ... }`` generates a function which
974updates the given fields in a record.
974updates the given fields in a record.
975
975
976+Each record is defined in its own namespace, which means that field names
977+can be reused in multiple records.
978+
976Records, and fields within records, can have dependent types. Updates
979Records, and fields within records, can have dependent types. Updates
977are allowed to change the type of a field, provided that the result is
980are allowed to change the type of a field, provided that the result is
978well-typed.
981well-typed.