revise example

rahxephon89 · rahxephon89 · commit 5a3281154f89 · 2025-01-23T09:17:59.000-08:00
diff --git a/apps/nextra/pages/en/build/smart-contracts/prover/spec-lang.mdx b/apps/nextra/pages/en/build/smart-contracts/prover/spec-lang.mdx
@@ -837,11 +837,11 @@ module 0x42::m {
 }
 ```
 
-Notice that type parameters are supported in global invariants. For example:
+Notice that type parameters are supported in global invariants. For example, the invariant above can be rewritten into the below one if `Counter` is generic:
 
 ```move
 module addr::M {
-    invariant<Y> forall addr: address where exists<R<Y>>(addr): exists<T<Y>>(addr);
+    invariant<T> forall a: addr where exists<Counter<T>>(a): global<Counter<T>>(a).value > 0;
 }
 ```
 

Original file line number	Diff line number	Diff line change
`@@ -837,11 +837,11 @@ module 0x42::m {`
`837`	`837`	`}`
`838`	`838`	```
`839`	`839`
`840`		`-Notice that type parameters are supported in global invariants. For example:`
	`840`	+Notice that type parameters are supported in global invariants. For example, the invariant above can be rewritten into the below one if `Counter` is generic:
`841`	`841`
`842`	`842`	```move
`843`	`843`	`module addr::M {`
`844`		`- invariant<Y> forall addr: address where exists<R<Y>>(addr): exists<T<Y>>(addr);`
	`844`	`+ invariant<T> forall a: addr where exists<Counter<T>>(a): global<Counter<T>>(a).value > 0;`
`845`	`845`	`}`
`846`	`846`	```
`847`	`847`