From 5caa19990b68a7eb7d25938fcfb96f714e2216e0 Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Fri, 1 Nov 2019 05:57:47 -0700 Subject: [PATCH] [sledge sem] Improve a comment Reviewed By: jberdine Differential Revision: D18269122 fbshipit-source-id: 9e9fba662 --- sledge/semantics/llairScript.sml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml index e6f15ced2..db943571a 100644 --- a/sledge/semantics/llairScript.sml +++ b/sledge/semantics/llairScript.sml @@ -215,9 +215,11 @@ Definition nfits_def: 0 < size ∧ n < 2 ** size End -(* Convert an integer to an unsigned number, following the 2's complement, - * assuming (ifits i size). This looks like what OCaml's Z.extract does, which - * is used in LLAIR for Convert expressions *) +(* Convert an integer to an unsigned number, following the 2's complement + * representation, assuming (ifits i size). This is what OCaml's Z.extract does, + * which is used in LLAIR for Convert expressions and unsigned operations, e.g., + * <. The difference between LLAIR's extract and i2n is that i2n assumes that i + * fits into size rather than truncating it first. *) Definition i2n_def: i2n (IntV i size) : num = if i < 0 then