From c0e1c408b582105153460f776aa67f038b33e9a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 11 May 2023 19:50:47 +0200 Subject: [PATCH] Update tutorial.md (#603) --- docs/tutorial.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/tutorial.md b/docs/tutorial.md index cace56515..d09f6bcf5 100644 --- a/docs/tutorial.md +++ b/docs/tutorial.md @@ -401,7 +401,7 @@ pure func toSeq(s []int) (res seq[int]) { Gobra supports many of Go's native types, namely integers (`int`, `int8`, `int16`, `int32`, `int64`, `byte`, `uint8`, `rune`, `uint16`, `uint32`, `uint64`, `uintptr`), strings, structs, pointers, arrays, slices, interfaces, and channels. Note that currently the support for strings and specific types of integers such as `rune` is very limited. -In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`|set1|`). +In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`len(set1)`). ## Interfaces @@ -680,4 +680,4 @@ java -Xss128m -jar gobra.jar -i [FILES_TO_VERIFY] To check the full list of flags available in Gobra, run the command ```bash java -jar gobra.jar -h -``` \ No newline at end of file +```