adc85d7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Minor edits to the tutorial

commitadc85d7c1475f413e099e8eca81f06b656e61f82 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 22 Mar 2016, 11:12 (11 years ago) parent172f0da

2 files changed+4−1

unifiedsplit

docs/tutorial/introduction.rst+1−1

@@ -39,7 +39,7 @@ function, which concatenates vectors:

3939This tutorial introduces Idris, a general purpose functional

4040programming language with dependent types. The goal of the Idris

4141project 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

4343language which aims to generate efficient executable code. It also has

4444a lightweight foreign function interface which allows easy interaction

4545with external ``C`` libraries.

docs/tutorial/typesfuns.rst+3

@@ -973,6 +973,9 @@ updated):

973973The syntax ``record { field = val, ... }`` generates a function which

974974updates the given fields in a record.

975975

976+Each record is defined in its own namespace, which means that field names

977+can be reused in multiple records.

978+

976979Records, and fields within records, can have dependent types. Updates

977980are allowed to change the type of a field, provided that the result is

978981well-typed.