From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 12:20:28 +0200
Subject: Improve the generated comments

---
 tests/hol4/misc-polonius_list/poloniusListScript.sml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/hol4/misc-polonius_list')

diff --git a/tests/hol4/misc-polonius_list/poloniusListScript.sml b/tests/hol4/misc-polonius_list/poloniusListScript.sml
index dd631169..06876ed4 100644
--- a/tests/hol4/misc-polonius_list/poloniusListScript.sml
+++ b/tests/hol4/misc-polonius_list/poloniusListScript.sml
@@ -11,7 +11,7 @@ Datatype:
 End
 
 val [get_list_at_x_fwd_def] = DefineDiv ‘
-  (** [polonius_list::get_list_at_x] *)
+  (** [polonius_list::get_list_at_x]: forward function *)
   get_list_at_x_fwd (ls : u32 list_t) (x : u32) : u32 list_t result =
     (case ls of
     | ListCons hd tl =>
@@ -20,7 +20,7 @@ val [get_list_at_x_fwd_def] = DefineDiv ‘
 ’
 
 val [get_list_at_x_back_def] = DefineDiv ‘
-  (** [polonius_list::get_list_at_x] *)
+  (** [polonius_list::get_list_at_x]: backward function 0 *)
   get_list_at_x_back
     (ls : u32 list_t) (x : u32) (ret : u32 list_t) : u32 list_t result =
     (case ls of
-- 
cgit v1.2.3