summaryrefslogtreecommitdiff
path: root/src/Expressions.ml
diff options
context:
space:
mode:
authorSon Ho2022-10-26 19:42:30 +0200
committerSon HO2022-10-26 19:45:09 +0200
commit16560ce5d6409e0f0326a0c6046960253e444ba4 (patch)
treec17058a7fb7e076134841271b7693ba18b1b9285 /src/Expressions.ml
parente1f79b07440f35e5e6296b61819cf50e6f60f090 (diff)
Update the code documentation to fix links and syntax issues
Diffstat (limited to 'src/Expressions.ml')
-rw-r--r--src/Expressions.ml20
1 files changed, 10 insertions, 10 deletions
diff --git a/src/Expressions.ml b/src/Expressions.ml
index bf06dd1e..e2eaf1e7 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -82,21 +82,21 @@ type operand =
Note that ADTs are desaggregated at some point in MIR. For instance, if
we have in Rust:
- ```
- let ls = Cons(hd, tl);
- ```
+ {[
+ let ls = Cons(hd, tl);
+ ]}
In MIR we have (yes, the discriminant update happens *at the end* for some
reason):
- ```
- (ls as Cons).0 = move hd;
- (ls as Cons).1 = move tl;
- discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
- ```
+ {[
+ (ls as Cons).0 = move hd;
+ (ls as Cons).1 = move tl;
+ discriminant(ls) = 0; // assuming [Cons] is the variant of index 0
+ ]}
Note that in our semantics, we handle both cases (in case of desaggregated
- initialization, `ls` is initialized to `⊥`, then this `⊥` is expanded to
- `Cons (⊥, ⊥)` upon the first assignment, at which point we can initialize
+ initialization, [ls] is initialized to [⊥], then this [⊥] is expanded to
+ [Cons (⊥, ⊥)] upon the first assignment, at which point we can initialize
the field 0, etc.).
*)
type aggregate_kind =