search

UoY-RoboStar / robochart-textual

This repository contains the plugins for the RoboChart textual editor
Eclipse Public License 2.0
0 stars 1 forks source link

Require a built-in function for square in RoboChart #67

Open uoy-fangyan opened 1 year ago

uoy-fangyan commented 1 year ago

Hi, I am wondering if it's possible to add a built-in function of 'square' or 'exponential' in RoboChart? I am doing a transformation from RoboChart to Z Machine notations, and ^ is defined as exponential in Isabelle/HOL. But there is no corresponding function in RoboChart.

pefribeiro commented 1 year ago

Hi @uoy-fangyan,

We've looked further into this and exponentiation is not part of the Z standard, although there is syntax for subscripts, therefore this should indeed be defined as a function.

Thanks, Pedro