Merge pull request #12 from Dev-XYS/predicate-tag

Change the label for subsection "Predicates"

tutorial/permissions.md

@@ -1,6 +1,6 @@
 # Permissions {#permissions}
 
-## Introduction
+## Introduction {#perm-introduction}
 
 Reasoning about the heap of a Viper program is governed by *field permissions*, which specify the heap locations that a statement, an expression or an assertion may access (read and/or modify).
 Heap locations can be accessed only if the corresponding permission is *held* by the currently verified method. The simplest form of field permission is the *exclusive* permission to a heap location `x.f`; it expresses that the current method may read and write to the location, whereas other methods or threads are not allowed to access it in any way.

tutorial/structure.md

@@ -46,7 +46,7 @@ method QSort(xs: Seq[Ref]) returns (ys: Seq[Ref])
   * The postcondition is assumed after the method call (more precisely, it is [_inhaled_](#inhaling-and-exhaling))
 * See the [permission section](#permissions) for more details and examples
 
-### Functions
+### Functions {#intro-functions}
 
 ```silver
 function gte(x: Ref, a: Int): Int
@@ -67,7 +67,7 @@ function gte(x: Ref, a: Int): Int
 * Unlike methods, function applications are not handled modularly (for functions with bodies): changing the body of a function affects client code
 * See the [section on functions](#functions) for details
 
-### Predicates
+### Predicates {#intro-predicates}
 
 ```silver
 predicate list(this: Ref) {