Remove reference to distinction between terms and formulae

ocaml-gospel · Dec 9, 2024 · 4d41ad0 · 4d41ad0
1 parent 8930a8d
commit 4d41ad0
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/docs/docs/language/expressions.md b/docs/docs/language/expressions.md
@@ -4,10 +4,6 @@ sidebar_position: 3
 
 # Expressions
 
-Gospel expression can be either a term (e.g. `x+1`) or a formula (e.g.
-`forall i. i > 2 -> f i > 0`). This distinction is made during type checking,
-and not at the syntax level.
-
 The syntax for Gospel expressions is largely OCaml's syntax.
 The main differences are: