Ursus language documentation

User types

Here is explained how to create your own structure via using Pruvendo tools. For example you want to create structures, which can be describe like:

struct Person {
    string name;
    string surName;
    uint age;
}

Ok, now we can create the folowing structure in Ursus:

Inductive PersonFields := 
| Person_ι_name 
| Person_ι_surName 
| Person_ι_age
.
Definition PersonL := [string : Type ; string : Type ; uint : Type]%glist.
GlobalGeneratePruvendoRecord PersonL PersonFields.

And using command GlobalGeneratePruvendoRecord we can create new type, which will be called in this example as PersonLRecord. Literal can be expressed like [{"John"}, {"Smith"}, {42}].

Finally, let's sat that way of expressing structures is not recomended, so it is better to use Contract command which expressed here