The following data structure is defined in HOL4.
val _ = Datatype `
my = <|
r: num;
b: num;
dis: real
|>`;
Given a mylist(:my list), if a
I recommend learning about the syntax of HOL a bit more. Also, as Michael
suggested (to you or someone else) maybe write the code up first as an SML
program and then translate to HOL. In any case, here are some nonsense
definitions that HOL allows. They should help you get further.
load
The following data types are defined in HOL4.val _ =
Datatype ` coordinate = <|
x_axis: real; y_axis: real;
z_axis: real
There seems to be some problems with the syntax. For one, the !ch ... on
the right hand side of the definition means that the rhs is boolean, which
conflicts with the record values being returned by the if-then-else.
Konrad.
On Wed, Dec 19, 2018 at 8:04 PM 幻＠未来 <849678...@qq.com> wrote:
> The
The following data types are defined in HOL4.val _ =
Datatype ` coordinate = <|
x_axis: real; y_axis: real;
z_axis: real
recommend trying to write your algorithm in
SML (or Haskell, or OCaml), and then translating it to HOL.
Michael
From: 幻＠未来 <849678...@qq.com>
Date: Thursday, 20 December 2018 at 12:38
To: hol-info
Subject: [Hol-info] Element assignment in structures
The following data types are d
The following data types are defined in HOL4.
val _ = Datatype ` coordinate = <|
x_axis: real;
y_axis: real; z_axis: real
Thank you for your answer. I made the following attempt in HOL4.
open realLib;
val _ = Datatype `
coordinate = <|
x_axis: real;
y_axis: real;
values.
Michael
From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 18 December 2018 at 13:57
To: hol-info
Subject: [Hol-info] Element assignment in structures
Hello!
I defined the following data structure in HOL4.
Datatype `
Hello!
I defined the following data structure in HOL4.
Datatype `
chromosome = <|
r: num;
b: num;
distance: real;
10 matches
Mail list logo
