diff options
| author | Son Ho | 2023-07-06 12:20:28 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-06 12:20:28 +0200 |
| commit | 7c95800cefc87fad894f8bf855cfc047e713b3a7 (patch) | |
| tree | 11b22541914a933bef896b5e765b002ac934faae /tests/hol4/misc-polonius_list | |
| parent | 5ca36bfc50083a01af2b7ae5f75993a520757ef5 (diff) | |
Improve the generated comments
Diffstat (limited to 'tests/hol4/misc-polonius_list')
| -rw-r--r-- | tests/hol4/misc-polonius_list/poloniusListScript.sml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |