Stream: Beginner Questions

Topic: Document about Isar Implementation

Qiyuan Xu (May 19 2022 at 06:38):

Hi guys, I'm developing some Isar components and I really need some documents about files under src/Pure/Isar to tell me what is the meaning of each parameter like, in 'src/Pure/Isar/expression.ML'

  (* Locale expressions *)
  datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
  type 'term rewrites = (Attrib.binding * 'term) list
  type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list
  type expression_i = (string, term) expr * (binding * typ option * mixfix) list
  type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list

Who can know the meaning of the boolean parameter and the string without a document... so... please...
I searched the implementation document but it tells nothing about this and other Isar components...

Qiyuan Xu (May 19 2022 at 06:55):

oh, god, I recognized those arguments coincide with the syntax given in isar_ref, so I can decode the meaning of them according to their order... oh okay... sorry for the disturbance but some further documents is still really appreciated (if there is).

Last updated: Apr 23 2024 at 04:18 UTC