Update Definition syntaxes to allow declaration of types of new constants

[mn200]

One possibility

Definition foo_def:
   (** constname1 : type1 *)
   (** constname2 : type2 *)
   ...
End

[konrad-slind]

multiDefine will support lists of definitions, so the proposed syntax could be more liberal.

…

On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish ***@***.***> wrote: One possibility Definition foo_def: (** constname1 : type1 *) (** constname2 : type2 *) ... End — Reply to this email directly, view it on GitHub <#1065>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[konrad-slind]

It also supports prim. rec defns. in the list: TotalDefn.multiDefine `(f2 0 = 3) /\ (f2 (SUC n) = 1 + f2 n) /\ (f3 0 = f2 0) /\ (f3 (SUC n) = f2 n + f2 n) /\ (f4 x = f2 x + f3 (f2 x))`;

…

On Wed, Oct 26, 2022 at 1:59 PM Konrad Slind ***@***.***> wrote: multiDefine will support lists of definitions, so the proposed syntax could be more liberal. On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish ***@***.***> wrote: > One possibility > > Definition foo_def: > (** constname1 : type1 *) > (** constname2 : type2 *) > ... > End > > — > Reply to this email directly, view it on GitHub > <#1065>, or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE> > . > You are receiving this because you are subscribed to this thread.Message > ID: ***@***.***> >

[konrad-slind]

And it supports wfrec defns when the auto-prover manages to solve the termination problem: TotalDefn.multiDefine `(f5 n = if n = 0n then 1 else n * f5 (n-1)) /\ (f6 [] = [] /\ f6 [[x]] = [x] /\ f6 (h::t) = h ++ f6 t)`;

…

On Wed, Oct 26, 2022 at 2:05 PM Konrad Slind ***@***.***> wrote: It also supports prim. rec defns. in the list: TotalDefn.multiDefine `(f2 0 = 3) /\ (f2 (SUC n) = 1 + f2 n) /\ (f3 0 = f2 0) /\ (f3 (SUC n) = f2 n + f2 n) /\ (f4 x = f2 x + f3 (f2 x))`; On Wed, Oct 26, 2022 at 1:59 PM Konrad Slind ***@***.***> wrote: > multiDefine will support lists of definitions, so the proposed syntax > could be more liberal. > > > On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish ***@***.***> > wrote: > >> One possibility >> >> Definition foo_def: >> (** constname1 : type1 *) >> (** constname2 : type2 *) >> ... >> End >> >> — >> Reply to this email directly, view it on GitHub >> <#1065>, or unsubscribe >> <https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE> >> . >> You are receiving this because you are subscribed to this thread.Message >> ID: ***@***.***> >> >

[konrad-slind]

And there is elaborate clique-finding etc so the order of the declarations doesn't matter. See https://github.com/HOL-Theorem-Prover/HOL/blob/2eff78b608efb12cbea315f4813b4f4af70793a0/src/tfl/src/Defn.sml#L1825 for where that stuff is implemented. It might be too elaborate ... I thought it was a good idea at the time. Konrad.

…

On Wed, Oct 26, 2022 at 2:08 PM Konrad Slind ***@***.***> wrote: And it supports wfrec defns when the auto-prover manages to solve the termination problem: TotalDefn.multiDefine `(f5 n = if n = 0n then 1 else n * f5 (n-1)) /\ (f6 [] = [] /\ f6 [[x]] = [x] /\ f6 (h::t) = h ++ f6 t)`; On Wed, Oct 26, 2022 at 2:05 PM Konrad Slind ***@***.***> wrote: > It also supports prim. rec defns. in the list: > > TotalDefn.multiDefine > `(f2 0 = 3) /\ > (f2 (SUC n) = 1 + f2 n) /\ > (f3 0 = f2 0) /\ > (f3 (SUC n) = f2 n + f2 n) /\ > (f4 x = f2 x + f3 (f2 x))`; > > > On Wed, Oct 26, 2022 at 1:59 PM Konrad Slind ***@***.***> > wrote: > >> multiDefine will support lists of definitions, so the proposed syntax >> could be more liberal. >> >> >> On Wed, Oct 26, 2022 at 4:39 AM Michael Norrish < >> ***@***.***> wrote: >> >>> One possibility >>> >>> Definition foo_def: >>> (** constname1 : type1 *) >>> (** constname2 : type2 *) >>> ... >>> End >>> >>> — >>> Reply to this email directly, view it on GitHub >>> <#1065>, or unsubscribe >>> <https://github.com/notifications/unsubscribe-auth/AAIOAD3755WCNHPSFGM7O5DWFD33RANCNFSM6AAAAAAROZTGNE> >>> . >>> You are receiving this because you are subscribed to this thread.Message >>> ID: ***@***.***> >>> >>