Boyer-Moore theory has "shells", which are like structures. See page 39 of [1]. Since this is a pure functional language, values cannot be altered. Shells have constructors, a type predicate, and can have restriction predicates on values.

    Shell Definition.
    Add the shell ADD1 of one argument
    with bottom object (ZERO),
    recognizer NUMBERP,
    accessor SUB1,
    type restriction (NUMBERP X1),
    default value (ZERO), and
    well-founded relation SUB1P.

It's not intended that you run programs in Boyer-Moore theory, although you can. It's a proof tool.

[1] https://www.cs.utexas.edu/users/boyer/acl.pdf