From f76be9afab885946f5ae4a7979afa6ef810280a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Roland=20Lei=C3=9Fa?= Date: Tue, 18 Feb 2025 01:38:53 +0100 Subject: [PATCH] docs --- docs/langref.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/docs/langref.md b/docs/langref.md index 7d3229dfbf..0e99c87cda 100644 --- a/docs/langref.md +++ b/docs/langref.md @@ -50,7 +50,6 @@ In addition the following keywords are _terminals_: | Terminal | Comment | | --------- | -------------------------------------------------------- | -| `.module` | starts a module | | `import` | imports another Mim file | | `plugin` | like `import` and additionally loads the compiler plugin | | `axm` | axiom | @@ -236,12 +235,12 @@ This will bind Here is another example: ```rust -{T: *, a: Nat} as Ts [%mem.M, %mem.Ptr Ts] → [%mem.M, T] +{T: *, a: Nat} as Ts → [%mem.M, %mem.Ptr Ts] → [%mem.M, T] ``` #### Rebind -A `let` and `ret` expression allows you to rebind the same name to a different value: +A `let` and `ret` expression allows you to rebind the same name to a different value. This is particularly useful, when dealing with memory: ```rust @@ -372,9 +371,9 @@ ret res = f Nat $ (23, 42); use(res) Finally, the following function types are all equivalent and denote the type of `f` above. ```rust -[T:*] → [[T, T], T → ⊥] → ⊥ -[T:*] → Cn [[T, T], Cn T] -[T:*] → Fn [T, T] → T +[T: *] → [[T, T], T → ⊥] → ⊥ +[T: *] → Cn [[T, T], Cn T] +[T: *] → Fn [T, T] → T ``` ## Scoping