Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
09 March 2024, 04:34:05 UTC
Revision 480c0ea6498bb31d7a24896588723f12fba9d97d authored by Pierre-Yves Strub on 28 August 2023, 15:37:04 UTC, committed by Pierre-Yves Strub on 06 September 2023, 13:42:47 UTC 
Operator unfolding when applied to enough arguments
 
When declaring an operator, it is now possible to specify which
arguments are mandatory before an operator application is
automtically unfolded during simplification.

Syntax is:

```
op name (x1 : t1) (xp : tp) / (x_p+1 : t_p+1) ... = ...
```

where the optional `/` indicated that the operator `name` will
be automatically unfolded when applied to at least `p`
arguments.
1 parent 8243791
Raw File
Tip revision: 480c0ea6498bb31d7a24896588723f12fba9d97d authored by Pierre-Yves Strub on 28 August 2023, 15:37:04 UTC
Operator unfolding when applied to enough arguments
Tip revision: 480c0ea
.dir-locals.el 
((tuareg-mode .
   ((require-final-newline . t)
    (c-basic-offset . 2)
    (tab-width . 2)
    (indent-tabs-mode . nil)
    (eval . (add-hook 'write-contents-functions 'delete-trailing-whitespace)))))
 (easycrypt-mode .
   ((require-final-newline . t)
    (indent-tabs-mode . nil)))
back to top