https://github.com/EasyCrypt/easycrypt
Revision 341cc08a8b8d23310b18b3587d1b5dacca7f6456 authored by Benjamin Gregoire on 26 October 2022, 18:18:55 UTC, committed by Pierre-Yves Strub on 16 June 2023, 10:39:43 UTC
We realized that sometimes we want to inline everything besides one procedure and found that it is cumbersome to have to list everything that has to be inlined instead of listing what should remain as is. So we decided to add this to the current inline. We should have kept the previous use cases identical as supported by the fact that nothing broke while not touching any old ec files. In doing so, we also added the possibility to provide the name of a module leading to inlining all the procedure in this module. Finally, one can now provide the name of a procedure and it will inline all the procedures with that name regardless of the module in which they belong. As already mentioned, one can find examples at the following link. https://github.com/EasyCrypt/easycrypt/blob/deploy-inline/examples/tactics/inline.ec start with parsing pattern matching on inline add some examples fix
1 parent f0e15c2
Tip revision: 341cc08a8b8d23310b18b3587d1b5dacca7f6456 authored by Benjamin Gregoire on 26 October 2022, 18:18:55 UTC
New inline tactic
New inline tactic
Tip revision: 341cc08
| File | Mode | Size |
|---|---|---|
| .github | ||
| config | ||
| examples | ||
| scripts | ||
| src | ||
| theories | ||
| .dir-locals.el | -rw-r--r-- | 285 bytes |
| .gitignore | -rw-r--r-- | 118 bytes |
| AUTHORS | -rw-r--r-- | 543 bytes |
| LICENSE | -rw-r--r-- | 1.2 KB |
| Makefile | -rw-r--r-- | 1.3 KB |
| README.md | -rw-r--r-- | 8.0 KB |
| default.nix | -rw-r--r-- | 921 bytes |
| dune | -rw-r--r-- | 221 bytes |
| dune-project | -rw-r--r-- | 450 bytes |
| easycrypt.opam | -rw-r--r-- | 1.2 KB |
| easycrypt.opam.template | -rw-r--r-- | 915 bytes |
| easycrypt.png | -rw-r--r-- | 182.6 KB |
| shell.nix | -rw-r--r-- | 741 bytes |
Computing file changes ...
