Skip to content

Commit

Permalink
docs
Browse files Browse the repository at this point in the history
  • Loading branch information
leissa committed Feb 18, 2025
1 parent 054347b commit f76be9a
Showing 1 changed file with 5 additions and 6 deletions.
11 changes: 5 additions & 6 deletions docs/langref.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit f76be9a

Please sign in to comment.