git.iko.soy/Idris-dev
on master help sign in
Fixed highlighting/indentation for code examples
2ca5558Ahmad Salim Al-Sibahi
CHANGELOG.md+3−3
compare with master
unifiedsplit
@@ -5,7 +5,7 @@
5* `record` syntax now allows updating fields, including nested fields,
5* `record` syntax now allows updating fields, including nested fields,
6 by applying a function using the `$=` operator. For example:
6 by applying a function using the `$=` operator. For example:
7
7
8− ```
8+ ```idris
9 record Score where
9 record Score where
10 constructor MkScore
10 constructor MkScore
11 correct : Nat
11 correct : Nat
@@ -23,9 +23,9 @@
23
23
24* Implicit parameter to interfaces are now allowed. For example:
24* Implicit parameter to interfaces are now allowed. For example:
25
25
26− ```
26+ ```idris
27 interface Shows (ts : Vect k Type) where
27 interface Shows (ts : Vect k Type) where
28− shows : HVect ts -> Vect k String
28+ shows : HVect ts -> Vect k String
29 ```
29 ```
30 In this interface, `k` is an implicit parameter, but previously needed to
30 In this interface, `k` is an implicit parameter, but previously needed to
31 be explicit
31 be explicit