diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index c015d4d2..00000000 --- a/.gitmodules +++ /dev/null @@ -1,3 +0,0 @@ -[submodule "agda-stdlib"] - path = agda-stdlib - url = https://github.com/agda/agda-stdlib.git diff --git a/README.md b/README.md index c241a715..b735455c 100644 --- a/README.md +++ b/README.md @@ -31,7 +31,7 @@ When run in a terminal, our demo will show a translation roundtrip, showcasing t Vatras is a library to study and compare meta-languages for specifying variability in source code and data. Some software systems are configurable _before_ they are compiled, i.e., statically. -A common way example for implementing static variability is by conditional compilation, as for example possible with the C preprocessor. +A common way to implement static variability is by conditional compilation, as for example possible with the C preprocessor. For instance, the following [code snippet from the Linux kernel](https://github.com/torvalds/linux/blob/e271ed52b344ac02d4581286961d0c40acc54c03/include/linux/console.h#L479-L486) ```C @@ -140,9 +140,9 @@ We tested our setup on Manjaro, NixOS, Windows Subsystem for Linux (WSL2), and w > In case of problems, there is a "Troubleshooting" section at the bottom of this file. ### Setup -Clone the library and its submodules to a directory of your choice: +Clone the library to a directory of your choice: ```shell -git clone --recursive https://github.com/VariantSync/Vatras.git +git clone https://github.com/VariantSync/Vatras.git ``` There are **three alternative ways** to compile the library and run its small demo. @@ -153,14 +153,14 @@ In general, we **recommend Nix** because it creates a sandbox environment with a - For **Mac** users, we recommend Nix or Docker. (We experienced problems with installing Agda manually.) - For **Linux** users, any alternative is fine but we recommend Nix for the reasons mentioned above. -There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose.. -The only dependency of our library is the Agda standard library which is shipped as a git submodule within the `agda-stdlib` directory and is taken care of automatically by our [makefile](makefile). +There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose. +The only dependency of our library is the Agda standard library which is automatically taken care of by our Nix and Docker setups. Note that building for the first time (or running `nix-shell`) will take a while because Agda has to build the required dependencies from the standard library (expect ~5-10min and a lot of terminal output). #### Alternative 1: Setup via Nix -The installation of Nix depends on your operating system. Head to the [NixOS website](https://nixos.org/download/) and follow the installation instructions for your system. Follow the download instructions for `Nix: the package manager`, not `NixOS: the Linux distribution`! Note that Nix is not directly available for Windows but it can be used from within Windows Subsystem for Linux (WSL2). When you open a WSL2 terminal terminal, you can install Nix by following the instructions for installing Nix on linux from the [NixOS website](https://nixos.org/download/). +The installation of Nix depends on your operating system. Head to the [NixOS website](https://nixos.org/download/) and follow the installation instructions for your system. Follow the download instructions for `Nix: the package manager`, not `NixOS: the Linux distribution`! Note that Nix is not directly available for Windows but it can be used from within Windows Subsystem for Linux (WSL2). When you open a WSL2 terminal, you can install Nix by following the instructions for installing Nix on Linux from the [NixOS website](https://nixos.org/download/). When you have Nix installed on your system, open a terminal, navigate to this directory, and then simply open a Nix shell by typing ```shell @@ -171,7 +171,7 @@ To compile the library and run the demo, simply run make: ```shell make ``` -The expected output is explained in detail in the Step-by-Step guide below. +The expected output is explained in detail in the [Expected Output section](#expected-output) below. Alternatively, the demo can be compiled locally to `./result/bin`. ```shell @@ -189,7 +189,7 @@ How to install Docker depends on your operating system. **For Windows or Mac**, Once you have installed Docker, start the Docker daemon. **On Windows**, open the search bar using the 'Windows Key' and search for 'Docker' or 'Docker Desktop'. **On Linux**, the docker daemon typically runs automatically, so there is nothing to do; otherwise, start Docker's service using your service manager (e.g., with `systemd`, execute `sudo systemctl start docker`). -More detailed instructions on starting the deamon are given [here](https://docs.docker.com/config/daemon/start/) on the docker website. +More detailed instructions on starting the deamon are given [on the docker website](https://docs.docker.com/config/daemon/start/). Afterwards, open a terminal and navigate to this repository's directory (the directory containing this README.md). First, you must create the docker image: @@ -210,7 +210,7 @@ docker run -t vatras #### Alternative 3: Manual Setup -The library needs Agda version 2.6.4.3 (newer version should also work but we did not test them). +The library needs Agda version 2.8.0 (newer version should also work but we did not test them). There are different ways to install Agda. Following the [Agda book's installation instructions], we recommend using [GHCup][ghcup] to install GHC, Cabal, and Agda as follows (You may skip steps for tools you have already installed but there might be compatibility errors with some versions): @@ -222,10 +222,10 @@ Following the [Agda book's installation instructions], we recommend using [GHCup 1. Install the GHC compiler and the cabal build tool with [GHCup][ghcup]. ```shell - ghcup install ghc 9.2.4 + ghcup install ghc 9.12.2 ghcup install cabal recommended - ghcup set ghc 9.2.4 + ghcup set ghc 9.12.2 ghcup set cabal recommended ``` @@ -233,16 +233,25 @@ Following the [Agda book's installation instructions], we recommend using [GHCup ```shell cabal update - cabal install Agda-2.6.4.3 + cabal install Agda-2.8.0 ``` To test whether the installation worked or whether your existing installation of Agda has the right version you can check the following command's output: ```shell > agda --version - Agda version 2.6.4.3 + Agda version 2.8.0 ``` + +3. Install the [Agda standard library](https://github.com/agda/agda-stdlib) version 2.3. + + ```shell + wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.3.tar.gz + tar -xzf agda-stdlib.tar.gz + mkdir -p "$(agda --print-agda-app-dir)" + realpath agda-stdlib-2.3/standard-library.agda-lib >> "$(agda --print-agda-app-dir)/libraries" + ``` -In case of confusion or trouble, we recommend to check the [official installation instructions](https://agda.readthedocs.io/en/v2.6.4.3/getting-started/installation.html), or follow the Getting-Started guide in the [Programming Language Foundations in Agda][plfa] book, or use the Nix setup, or check the troubleshooting instructions at the bottom of this file. +In case of confusion or trouble, we recommend to check the [official installation instructions](https://agda.readthedocs.io/en/v2.8.0/getting-started/installation.html), or follow the Getting-Started guide in the [Programming Language Foundations in Agda][plfa] book, or use the Nix setup, or check the troubleshooting instructions at the bottom of this file. To test whether your setup is correct, and to run the demo you may use our makefile. Make sure your terminal is in full-screen because the demo assumes to have at least 100 characters of horizontal space in the terminal for pretty-printing. @@ -251,28 +260,12 @@ Then run make ``` which will compile the library and run its small demo. -The expected output is explained in detail in the Step-by-Step guide below. - -## Step-by-Step Guide - -The "Kick-The-Tires" section above basically explains all necessary steps to get the library up and running. -Here, we give additional instructions on the expected output and how to play with other demo inputs. -For using the library once you finished the setup, please have a look at the later _Reusability Guide_, which, among other -information, includes an overview of the library, notes on our mechanized proofs, and tutorials for getting to know the library. - -### How does the demo know which standard library to use? - -Agda looks for its dependencies in a directory specified by the environment variable `AGDA_DIR`. The provided [makefile](makefile) sets this environment variable temporarily and locally during the build process to the `.libs` directory within this repository. (Your global setup will not be affected). If you want to run `agda` manually, or if you want to work on this project in an editor (e.g., emacs) then you have to set this environment variable to the libs directory in this repository. - -```shell -export AGDA_DIR="path/to/this/repository/libs" -``` +The expected output is explained in detail in the [Expected Output section](#expected-output) below. -Beware that setting the variable will overwrite any previously set directory. In that case you might want to overwrite the variable only temporarily while working on this project. -### Expected Output +#### Expected Output -The demo will print a long terminal output of about 1250 lines. +The demo will print a long terminal output of very rougly 1000 lines. A copy of the expected output can be found in the [expected-output.txt](expected-output.txt). First, the demo prints unicode characters to terminal, as a test for you to see whether your terminal supports unicode. @@ -358,9 +351,21 @@ Then add your new list to the `examples` list at the bottom of the file. ### Using our library in your own Agda projects +In order to use Vatras in your project, you need to state `Vatras` as a dependency in your Agda library file. +An Agda library file has the suffix `.agda-lib` and is usually contained in the root directory of your project. +Its content, including the dependency to Vatras, should include the following: +``` +name: YOUR-PROJECT-NAME +depend: Vatras +include: SOME/PATH/IN/YOUR/PROJECT +``` +For details about Agda's library management, please have a look at [Agda's packaging guide](https://agda.readthedocs.io/en/v2.8.0/tools/package-system.html). + +Afterwards, you need to follow one of the following alternatives to let Agda know where to find Vatras. + #### Alternative 1: Installation via Nix -When using Nix, you can use this repository as a library in you own project, by using `agda.withPackages`: +When using Nix, you can install this repository as an Agda library by using `agda.withPackages`: ```nix agda = nixpkgs.agda.withPackages [ nixpkgs.agdaPackages.standard-library @@ -373,19 +378,13 @@ Though, not required, we recommend to use the [nixpkgs pin](nix/sources.json) cr #### Alternative 2: Manual installation -After downloading this library, you can register it by appending the path of [Vatras.agda-lib](Vatras.agda-lib) to the file `$AGDA_DIR/libraries`, creating it if necessary. -If the environment variable `AGDA_DIR` is unset, it defaults to `~/.agda` on unix-like systems and `C:\Users\USERNAME\AppData\Roaming\agda` or similar on Windows. -After registering this library on your system, you can use it in your project by stating `Vatras` as a dependency in your Agda library file. -An Agda library file has the suffix `.agda-lib` and is usually contained in the root directory of your project. -Its content, including the dependency to Vatras, should include the following: - -``` -name: YOUR-PROJECT-NAME -depend: Vatras -include: SOME/PATH/IN/YOUR/PROJECT +After downloading this library, you can register it using the following commands: +```shell +mkdir -p "$(agda --print-agda-app-dir)" +realpath Vatras.agda-lib >> "$(agda --print-agda-app-dir)/libraries" ``` - -For details about Agda's library management, please have a look at [Agda's packaging guide](https://agda.readthedocs.io/en/v2.6.4.3/tools/package-system.html). +Make sure that you also have the Agda standard library version 2.3 installed. +See step 3 in the [manual setup](#alternative-3-manual-setup) for details on how to install ths Agda standard library. ### Notes on Mechanized Proofs @@ -593,15 +592,24 @@ during a Docker build, you might have encountered an out of memory issue. Try to rerun the same command after closing other applications which might comsume a lot of RAM. In some cases it may also be necessary to disable some kind of out-of-memory killer (also known as OOM killer or OOM deamon) but use this option with caution. -### Failed to read library file ./libs/../agda-stdlib/standard-library.agda-lib. -The following error may occur when executing `make` after a manual setup: +### Docker fails to open Git repository + +If you see an error like ``` -Failed to read library file ./libs/../agda-stdlib/standard-library.agda-lib. -Reason: ./libs/../agda-stdlib/standard-library.agda-lib: openBinaryFile: does not exist (No such file or directory) -make: *** [makefile:15: build] Error 42 +error: opening Git repository '"/home/user"': failed to resolve path '/home/your-user-name/some/path/.git/worktrees/Vatras': No such file or directory +------ +Dockerfile:19 +-------------------- + 17 | + 18 | # Verify all proofs and build the demo. + 19 | >>> RUN nix-build + 20 | + 21 | # Copy the demo with all runtime dependencies (ignoring build-time dependencies) +-------------------- +ERROR: failed to solve: process "/bin/sh -c nix-build" did not complete successfully: exit code: 1 ``` -This error indicates that the `agda-stdlib` git submodule has not been set up correctly. -Executing `git submodule update --init` in the root of the repository should fix the problem. +you may be in a Git worktree or your Git directory is out of place for some other reason. +Ensure that `git rev-parse --path-format=absolute --git-common-dir` (the path of the Git repository's data) is in your current working directory by creating a fresh non-bare clone without creating a second Git worktree. ## Where does the library name 'Vatras' come from? @@ -609,7 +617,7 @@ The name Vatras is (of course) an acronym, which stands for _VAriability languag Besides, Vatras is a water mage in the classic german RPG [Gothic II](https://almanach.worldofgothic.de/index.php/Vatras), who stems from the city of Varant, which almost sounds like _Variant_. Vatras is praying to the god Adanos, who brings some kind of equality or balance loosely speaking. -[agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.6.4.3-blue.svg -[agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.6.4.3 +[agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.8.0-blue.svg +[agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.8.0 [ghcup]: https://www.haskell.org/ghcup/ [plfa]: https://plfa.github.io/GettingStarted/ diff --git a/Vatras.agda-lib b/Vatras.agda-lib index 2475cba4..1cfea5f3 100644 --- a/Vatras.agda-lib +++ b/Vatras.agda-lib @@ -1,4 +1,4 @@ name: Vatras -depend: standard-library-2.0 +depend: standard-library-2.3 include: src flags: --sized-types diff --git a/agda-stdlib b/agda-stdlib deleted file mode 160000 index 2b8fff10..00000000 --- a/agda-stdlib +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 2b8fff10f4033b91a6df4007e4a65cb10047c89c diff --git a/expected-output.txt b/expected-output.txt index ea0c7728..fb4c732f 100644 --- a/expected-output.txt +++ b/expected-output.txt @@ -1,4 +1,5 @@ -It's dangerous to go alone! Take this unicode to see whether your terminal supports it: + +It's dangerous to go alone! Take this unicode to see whether your terminal supports it: โ‚™ โ‚ โ‚‚ ๐•ƒ โ„‚ ๐”ธ โŸฆ โŸง โŸจ โŸฉ โฒโณ ... but now on to the demo. @@ -280,7 +281,7 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ - โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ Experiment: Configure FST example โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ + โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ Experiment: Configuration FST example โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ Example: add-sub โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ @@ -410,6 +411,19 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ”‚ โ”‚ translate โ”‚ โ”‚ โ”‚ โ”‚ โ†“ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ 2CC w/o idempotent choices โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.DโŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ l, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ r โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ proven to have the same semantics as the previous expression โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ translate โ”‚ โ”‚ + โ”‚ โ”‚ โ†“ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ADT โ”‚ โ”‚ โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ 0.DโŸจ โ”‚ โ”‚ โ”‚ @@ -451,54 +465,54 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€ Example: Sandwich Recipe โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ CCC, original expression โ”‚ โ”‚ - โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง† โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ translate โ”‚ โ”‚ โ”‚ โ”‚ โ†“ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ NCC โ”‚ โ”‚ - โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง† โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ โ”‚ โ”‚ proven to have the same semantics as the previous expression โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ @@ -506,41 +520,41 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ”‚ โ†“ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ NCC โ”‚ โ”‚ - โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง† โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ โ”‚ โ”‚ proven to have the same semantics as the previous expression โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ @@ -548,41 +562,71 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ”‚ โ†“ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ 2CC โ”‚ โ”‚ - โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง† โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ proven to have the same semantics as the previous expression โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ translate โ”‚ โ”‚ + โ”‚ โ”‚ โ†“ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ 2CC w/o idempotent choices โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง† โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ โ”‚ โ”‚ proven to have the same semantics as the previous expression โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ @@ -590,198 +634,54 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ”‚ โ†“ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ADT โ”‚ โ”‚ - โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread--, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Salad?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, meat, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Patty?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ฮต>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, ketchup>-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Salad?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ฮต>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ๐Ÿฅš>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ฮต>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ๐Ÿฅš>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Patty?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ฮต>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ๐Ÿฅš>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 0.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ฮต>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 1.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ๐Ÿฅš>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ 2.Sauce?โŸจ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…>-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ โ”‚ โ”‚ proven to have the same semantics as the previous expression โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ @@ -789,73 +689,25 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ”‚ โ†“ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ VariantList โ”‚ โ”‚ - โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ [ Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, meat, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ฮต>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ , Bread-<ฮต, cheese, tofu, mayo+ketchup>- โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ] โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ [ ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ฮต>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ฮต>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<๐Ÿฅ—, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ฮต>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿ–, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ฮต>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ , ๐Ÿž-<ฮต, ๐Ÿง€, ๐Ÿง†, ๐Ÿ…๐Ÿฅš>- โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ] โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ โ”‚ โ”‚ proven to have the same semantics as the previous expression โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ @@ -865,389 +717,101 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo โ”‚ โ”‚ CCC โ”‚ โ”‚ โ”‚ โ”‚ โ•ญโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฎ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ default featureโŸจ โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ salad, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ… โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ… โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ meat, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅ—, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ… โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ–, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿฅš โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ ketchup โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ… โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >-, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ Bread-< โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿž-< โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ ฮต, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ cheese, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ tofu, โ”‚ โ”‚ โ”‚ - โ”‚ โ”‚ โ”‚ mayo+ketchup โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง€, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿง†, โ”‚ โ”‚ โ”‚ + โ”‚ โ”‚ โ”‚ ๐Ÿ…๐Ÿฅš โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ >- โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โŸฉ โ”‚ โ”‚ โ”‚ โ”‚ โ”‚ โ•ฐโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ•ฏ โ”‚ โ”‚ diff --git a/makefile b/makefile index ab294578..6398a474 100644 --- a/makefile +++ b/makefile @@ -1,21 +1,18 @@ -.PHONY: andrun check check-all check-everything build build-2.6.4.3 run clean +.PHONY: andrun check check-all check-everything build run clean andrun : build run check: - env AGDA_DIR="./libs" agda src/Vatras/Main.agda + agda src/Vatras/Main.agda check-all: ./scripts/check-all.sh check-everything: src/Vatras/Everything.agda - env AGDA_DIR="./libs" agda src/Vatras/Everything.agda + agda src/Vatras/Everything.agda build: - env AGDA_DIR="./libs" agda --compile src/Vatras/Main.agda - -build-2.6.4.3: - env AGDA_DIR="./libs" agda-2.6.4.3 --compile src/Vatras/Main.agda + agda --compile src/Vatras/Main.agda run: ./src/Main diff --git a/nix/sources.json b/nix/sources.json index 05a914cc..6e47a00a 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -5,10 +5,10 @@ "homepage": null, "owner": "NixOS", "repo": "nixpkgs", - "rev": "fd281bd6b7d3e32ddfa399853946f782553163b5", - "sha256": "1hy81yj2dcg6kfsm63xcqf8kvigxglim1rcg1xpmy2rb6a8vqvsj", + "rev": "cf3f5c4def3c7b5f1fc012b3d839575dbe552d43", + "sha256": "0rvzsqn8qk46mw80apwr14m9crc6a1rv404r7zshy1aq82plmbsc", "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/fd281bd6b7d3e32ddfa399853946f782553163b5.tar.gz", + "url": "https://github.com/NixOS/nixpkgs/archive/cf3f5c4def3c7b5f1fc012b3d839575dbe552d43.tar.gz", "url_template": "https://github.com///archive/.tar.gz" } } diff --git a/src/Vatras/Framework/Variants.agda b/src/Vatras/Framework/Variants.agda index b1c2780b..3e910f8d 100644 --- a/src/Vatras/Framework/Variants.agda +++ b/src/Vatras/Framework/Variants.agda @@ -146,7 +146,7 @@ module _ (V : ๐•) (A : ๐”ธ) {L : VariabilityLanguage V} (encoder : VariantEnc -- atom containment open import Relation.Nullary.Decidable using (yes; no) open import Data.Bool using (Bool; true) -open import Data.List using (or) +open import Data.Bool.ListAction using (or) has-atom : โˆ€ {A i} โ†’ atoms A โ†’ Rose i A โ†’ Bool has-atom {A , _โ‰Ÿ_} a (b -< cs >-) with a โ‰Ÿ b diff --git a/src/Vatras/Lang/ADT/Merge.agda b/src/Vatras/Lang/ADT/Merge.agda index eb82a526..01a1d54f 100644 --- a/src/Vatras/Lang/ADT/Merge.agda +++ b/src/Vatras/Lang/ADT/Merge.agda @@ -9,8 +9,6 @@ open import Data.Bool.Properties using (if-float) open import Relation.Binary.PropositionalEquality using (refl; _โ‰ก_; _โ‰—_) open Relation.Binary.PropositionalEquality.โ‰ก-Reasoning -open import Vatras.Util.AuxProofs using (if-cong) - import Vatras.Lang.ADT module Named (F : ๐”ฝ) where diff --git a/src/Vatras/Lang/ADT/Pushdown.agda b/src/Vatras/Lang/ADT/Pushdown.agda index de90b147..654aadf9 100644 --- a/src/Vatras/Lang/ADT/Pushdown.agda +++ b/src/Vatras/Lang/ADT/Pushdown.agda @@ -48,7 +48,7 @@ push-down-artifact {A = A} a cs = go cs [] (if config d then โŸฆ go a cs (cโ‚ โˆท cs') vs โŸง config else โŸฆ go a cs (cโ‚‚ โˆท cs') vs โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config d then_else_) (go' (cโ‚ โˆท cs') vs) (go' (cโ‚‚ โˆท cs') vs) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (go' (cโ‚ โˆท cs') vs) (go' (cโ‚‚ โˆท cs') vs) โŸฉ (if config d then a -< vs สณ++ List.map (ฮป e โ†’ โŸฆ e โŸง config) (cโ‚ โˆท cs') >- else a -< vs สณ++ List.map (ฮป e โ†’ โŸฆ e โŸง config) (cโ‚‚ โˆท cs') >-) diff --git a/src/Vatras/Show/Lines.agda b/src/Vatras/Show/Lines.agda index e39eb457..d118ecb9 100644 --- a/src/Vatras/Show/Lines.agda +++ b/src/Vatras/Show/Lines.agda @@ -7,6 +7,7 @@ open import Data.Bool using (true; false; if_then_else_; _โˆง_) open import Data.Char as Char using (Char) open import Data.Nat using (โ„•; _*_; _โˆธ_; โŒŠ_/2โŒ‹; โŒˆ_/2โŒ‰; _โ‰คแต‡_) open import Data.List as List using (List; _โˆท_; [_]; concat; splitAt; _โˆทสณ_) +open import Data.Nat.ListAction using (sum) open import Data.Maybe using (nothing; just) open import Data.String using (String; _++_; _==_; replicate; fromChar; toList; fromList; Alignment; fromAlignment) open import Data.Product as Prod using (_,_; projโ‚; mapโ‚) @@ -48,7 +49,7 @@ charWidth c = codePoint = Char.toโ„• c stringLength : String โ†’ โ„• -stringLength line = List.sum (List.map charWidth (Data.String.toList line)) +stringLength line = sum (List.map charWidth (Data.String.toList line)) length : Line โ†’ โ„• length line = stringLength (content line) diff --git a/src/Vatras/Translation/Lang/2CC-to-ADT.agda b/src/Vatras/Translation/Lang/2CC-to-ADT.agda index ba43781e..1d740206 100644 --- a/src/Vatras/Translation/Lang/2CC-to-ADT.agda +++ b/src/Vatras/Translation/Lang/2CC-to-ADT.agda @@ -10,6 +10,7 @@ module Vatras.Translation.Lang.2CC-to-ADT where open import Size using (Size; โˆž) import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Bool as Bool using (if_then_else_) +import Data.Bool.Properties as Bool open import Data.List as List using (List; []; _โˆท_; _สณ++_) import Data.List.Properties as List open import Vatras.Framework.Compiler using (LanguageCompiler) @@ -59,7 +60,7 @@ preserves-โ‰— (d โŸจ l , r โŸฉ) config = ADT.โŸฆ d โŸจ translate l , translate r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config d then ADT.โŸฆ translate l โŸง config else ADT.โŸฆ translate r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config d then_else_) (preserves-โ‰— l config) (preserves-โ‰— r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โ‰— l config) (preserves-โ‰— r config) โŸฉ 2CC.โŸฆ d โŸจ l , r โŸฉ โŸง config โˆŽ diff --git a/src/Vatras/Translation/Lang/2CC/Idempotence.agda b/src/Vatras/Translation/Lang/2CC/Idempotence.agda index de305e44..4efc6f1b 100644 --- a/src/Vatras/Translation/Lang/2CC/Idempotence.agda +++ b/src/Vatras/Translation/Lang/2CC/Idempotence.agda @@ -60,7 +60,7 @@ eliminate-idempotent-choices-preserves (a -< cs >-) c = eliminate-idempotent-choices-preserves (D โŸจ l , r โŸฉ) c with eliminate-idempotent-choices l โ‰Ÿ eliminate-idempotent-choices r eliminate-idempotent-choices-preserves (D โŸจ l , r โŸฉ) c | no lโ‰ขr = (if c D then โŸฆ eliminate-idempotent-choices l โŸง c else โŸฆ eliminate-idempotent-choices r โŸง c) - โ‰กโŸจ Eq.congโ‚‚ (if c D then_else_) (eliminate-idempotent-choices-preserves l c) (eliminate-idempotent-choices-preserves r c) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (eliminate-idempotent-choices-preserves l c) (eliminate-idempotent-choices-preserves r c) โŸฉ (if c D then โŸฆ l โŸง c else โŸฆ r โŸง c) โ‰กโŸจโŸฉ โŸฆ D โŸจ l , r โŸฉ โŸง c diff --git a/src/Vatras/Translation/Lang/2CC/Rename.agda b/src/Vatras/Translation/Lang/2CC/Rename.agda index bfa07749..2cbbfa4a 100644 --- a/src/Vatras/Translation/Lang/2CC/Rename.agda +++ b/src/Vatras/Translation/Lang/2CC/Rename.agda @@ -67,7 +67,7 @@ preserves-โŠ† f (d โŸจ l , r โŸฉ) config = 2CC.โŸฆ f d โŸจ rename f l , rename f r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config (f d) then 2CC.โŸฆ rename f l โŸง config else 2CC.โŸฆ rename f r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config (f d) then_else_) (preserves-โŠ† f l config) (preserves-โŠ† f r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ† f l config) (preserves-โŠ† f r config) โŸฉ (if config (f d) then 2CC.โŸฆ l โŸง (config โˆ˜ f) else 2CC.โŸฆ r โŸง (config โˆ˜ f)) โ‰กโŸจโŸฉ 2CC.โŸฆ d โŸจ l , r โŸฉ โŸง (config โˆ˜ f) @@ -96,11 +96,9 @@ preserves-โŠ‡ f fโปยน is-inverse (d โŸจ l , r โŸฉ) config = 2CC.โŸฆ d โŸจ l , r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config d then 2CC.โŸฆ l โŸง config else 2CC.โŸฆ r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config d then_else_) (preserves-โŠ‡ f fโปยน is-inverse l config) (preserves-โŠ‡ f fโปยน is-inverse r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ‡ f fโปยน is-inverse l config) (preserves-โŠ‡ f fโปยน is-inverse r config) โŸฉ (if config d then 2CC.โŸฆ rename f l โŸง (config โˆ˜ fโปยน) else 2CC.โŸฆ rename f r โŸง (config โˆ˜ fโปยน)) - โ‰กโŸจ Eq.cong (if_then 2CC.โŸฆ rename f l โŸง (config โˆ˜ fโปยน) else 2CC.โŸฆ rename f r โŸง (config โˆ˜ fโปยน)) - (Eq.cong config - (Eq.sym (is-inverse d))) โŸฉ + โ‰กโŸจ Bool.if-cong (Eq.cong config (Eq.sym (is-inverse d))) โŸฉ (if (config โˆ˜ fโปยน) (f d) then 2CC.โŸฆ rename f l โŸง (config โˆ˜ fโปยน) else 2CC.โŸฆ rename f r โŸง (config โˆ˜ fโปยน)) โ‰กโŸจโŸฉ 2CC.โŸฆ f d โŸจ rename f l , rename f r โŸฉ โŸง (config โˆ˜ fโปยน) diff --git a/src/Vatras/Translation/Lang/ADT-to-2CC.agda b/src/Vatras/Translation/Lang/ADT-to-2CC.agda index e92517fa..8ea0050a 100644 --- a/src/Vatras/Translation/Lang/ADT-to-2CC.agda +++ b/src/Vatras/Translation/Lang/ADT-to-2CC.agda @@ -47,7 +47,7 @@ preserves-โ‰— Variantโ†’2CC (f โŸจ l , r โŸฉ) config = 2CC.โŸฆ f โŸจ translate Variantโ†’2CC l , translate Variantโ†’2CC r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config f then 2CC.โŸฆ translate Variantโ†’2CC l โŸง config else 2CC.โŸฆ translate Variantโ†’2CC r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config f then_else_) (preserves-โ‰— Variantโ†’2CC l config) (preserves-โ‰— Variantโ†’2CC r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โ‰— Variantโ†’2CC l config) (preserves-โ‰— Variantโ†’2CC r config) โŸฉ (if config f then ADT.โŸฆ l โŸง config else ADT.โŸฆ r โŸง config) โ‰กโŸจโŸฉ ADT.โŸฆ f โŸจ l , r โŸฉ โŸง config diff --git a/src/Vatras/Translation/Lang/ADT-to-NADT.agda b/src/Vatras/Translation/Lang/ADT-to-NADT.agda index 7e5d1fbb..31559c37 100644 --- a/src/Vatras/Translation/Lang/ADT-to-NADT.agda +++ b/src/Vatras/Translation/Lang/ADT-to-NADT.agda @@ -54,7 +54,7 @@ preserves-โŠ† (f โŸจ l , r โŸฉ) config = NADT.โŸฆ if fnoc config f then translate l else translate r โŸง config โ‰กโŸจ Bool.if-float (ฮป e โ†’ NADT.โŸฆ e โŸง config) (fnoc config f) โŸฉ (if fnoc config f then NADT.โŸฆ translate l โŸง config else NADT.โŸฆ translate r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if fnoc config f then_else_) (preserves-โŠ† l config) (preserves-โŠ† r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ† l config) (preserves-โŠ† r config) โŸฉ (if fnoc config f then ADT.โŸฆ l โŸง (fnoc config) else ADT.โŸฆ r โŸง (fnoc config)) โ‰กโŸจโŸฉ ADT.โŸฆ f โŸจ l , r โŸฉ โŸง (fnoc config) @@ -71,7 +71,7 @@ preserves-โŠ‡ (f โŸจ l , r โŸฉ) config = ADT.โŸฆ f โŸจ l , r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config f then ADT.โŸฆ l โŸง config else ADT.โŸฆ r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config f then_else_) (preserves-โŠ‡ l config) (preserves-โŠ‡ r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ‡ l config) (preserves-โŠ‡ r config) โŸฉ (if config f then NADT.โŸฆ translate l โŸง (conf config) else NADT.โŸฆ translate r โŸง (conf config)) โ‰กโŸจ Bool.if-float (ฮป e โ†’ NADT.โŸฆ e โŸง (conf config)) (config f) โŸจ NADT.โŸฆ if config f then translate l else translate r โŸง (conf config) diff --git a/src/Vatras/Translation/Lang/ADT-to-VT.agda b/src/Vatras/Translation/Lang/ADT-to-VT.agda index 59565235..60804850 100644 --- a/src/Vatras/Translation/Lang/ADT-to-VT.agda +++ b/src/Vatras/Translation/Lang/ADT-to-VT.agda @@ -6,6 +6,7 @@ open import Vatras.Framework.Definitions using (๐”ฝ) module Vatras.Translation.Lang.ADT-to-VT (F : ๐”ฝ) where open import Data.Bool using (if_then_else_) +open import Data.Bool.Properties using (if-congโ‚‚) open import Data.List using (List; []; _โˆท_; _++_) open import Data.List.Properties using (++-identityสณ) open import Function using (id; _โˆ˜_) @@ -25,7 +26,6 @@ open import Vatras.Lang.VT.Encode F using (encode-forest; encode-forest-preserve open import Vatras.Framework.Relation.Expressiveness Forest using (_โ‰ฝ_; expressiveness-from-compiler) open import Vatras.Translation.Lang.ADT.ADT-vs-PropADT F Forest using (lift-compiler; ADTโ‰ฝPropADT) -open import Vatras.Util.AuxProofs using (if-cong) translate' : โˆ€ {A} โ†’ PropADT A โ†’ List (UnrootedVT A) translate' (leaf v) = encode-forest v @@ -40,7 +40,7 @@ preserves (D โŸจ l , r โŸฉ) c = โŸฆ D โŸจ l , r โŸฉ โŸงโ‚š c โ‰กโŸจโŸฉ (if eval D c then โŸฆ l โŸงโ‚š c else โŸฆ r โŸงโ‚š c) - โ‰กโŸจ if-cong (eval D c) (preserves l c) (preserves r c) โŸฉ + โ‰กโŸจ if-congโ‚‚ (eval D c) (preserves l c) (preserves r c) โŸฉ (if eval D c then configure-all (translate' l) c else configure-all (translate' r) c) โ‰กโŸจ ++-identityสณ _ โŸจ (if eval D c then configure-all (translate' l) c else configure-all (translate' r) c) ++ [] diff --git a/src/Vatras/Translation/Lang/ADT-to-VariantList.agda b/src/Vatras/Translation/Lang/ADT-to-VariantList.agda index 2ef24b1c..e79d59c3 100644 --- a/src/Vatras/Translation/Lang/ADT-to-VariantList.agda +++ b/src/Vatras/Translation/Lang/ADT-to-VariantList.agda @@ -17,6 +17,7 @@ open import Function using (_โˆ˜_) open import Data.List using (List; []; _โˆท_) open import Data.List.NonEmpty using (Listโบ; _โˆท_; _โบ++โบ_; length) +open import Data.List.NonEmpty.Properties using (length-โบ++โบ; length-โบ++โบ-โ‰คหก) open import Data.Nat using (โ„•; zero; suc; _+_; _โˆธ_; _<_; _โ‰ค?_; zโ‰คn; sโ‰คs) open import Data.Nat.Properties using (โ‰ค-trans; โ‰ฐโ‡’>; mโ‰คm+n; +-monoสณ-<) open import Data.Product using (_,_) @@ -42,7 +43,7 @@ open import Vatras.Lang.ADT.Path F V _==_ open import Vatras.Translation.Lang.ADT.DeadElim F V _==_ as DeadElim using (node; kill-dead; โŸฆ_โŸงแตค; UndeadADT; UndeadADTL) open import Vatras.Translation.Lang.ADT.WalkSemantics F V _==_ as Walk using () -open import Vatras.Util.List using (find-or-last; โบ++โบ-length; โบ++โบ-length-โ‰ค; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-โˆธ) +open import Vatras.Util.List using (find-or-last; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-โˆธ) {- This translates a ADT to a VariantList. @@ -81,7 +82,7 @@ conf-bounded : โˆ€ {A} โ†’ (c : PathConfig e) โ†’ conf e c < length (tr e) conf-bounded (leaf v) (.[] is-valid tleaf) = sโ‰คs zโ‰คn -conf-bounded (D โŸจ l , r โŸฉ) ((.D โ†ฃ true โˆท p) is-valid walk-left t) = โ‰ค-trans (conf-bounded l (p is-valid t)) (โบ++โบ-length-โ‰ค (tr l) (tr r)) +conf-bounded (D โŸจ l , r โŸฉ) ((.D โ†ฃ true โˆท p) is-valid walk-left t) = โ‰ค-trans (conf-bounded l (p is-valid t)) (length-โบ++โบ-โ‰คหก (tr l) (tr r)) conf-bounded (D โŸจ l , r โŸฉ) ((.D โ†ฃ false โˆท p) is-valid walk-right t) = go where c = p is-valid t @@ -96,7 +97,7 @@ conf-bounded (D โŸจ l , r โŸฉ) ((.D โ†ฃ false โˆท p) is-valid walk-right t) = go -- use the sum rule for โบ++โบ on the right hand side go : length (tr l) + conf r c < length (tr l โบ++โบ tr r) - go rewrite โบ++โบ-length (tr l) (tr r) = gox + go rewrite length-โบ++โบ (tr l) (tr r) = gox preservation-walk-to-list-conf : โˆ€ {A : ๐”ธ} โ†’ (e : ADT A) diff --git a/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda b/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda index 27c31417..81a875d9 100644 --- a/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda +++ b/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda @@ -2,6 +2,7 @@ open import Vatras.Framework.Definitions using (๐”ฝ; ๐•; ๐”ธ) module Vatras.Translation.Lang.ADT.ADT-vs-PropADT (F : ๐”ฝ) (V : ๐•) where open import Data.Bool using (if_then_else_; not) renaming (_โˆง_ to _and_) +open import Data.Bool.Properties using (if-not; if-โˆง; if-congโ‚‚; if-cong-then) open import Data.Product using (_,_) open import Function using (id; _โˆ˜_) open import Relation.Binary.PropositionalEquality as Eq using (_โ‰—_; refl) @@ -15,7 +16,6 @@ open ADT hiding (โŸฆ_โŸง) open import Vatras.Data.EqIndexedSet using (โ‰—โ†’โ‰…[]) open import Vatras.Data.Prop open import Vatras.Lang.ADT.Prop F V using (โŸฆ_โŸงโ‚š; PropADTL) -open import Vatras.Util.AuxProofs using (if-flip; if-โˆง; if-cong; if-congหก) open import Vatras.Framework.Compiler using (LanguageCompiler) open import Vatras.Framework.Relation.Expressiveness V using (_โ‰‹_; _โ‰ฝ_; expressiveness-from-compiler) @@ -57,7 +57,7 @@ elim-sem P l r c = if eval P c then โŸฆ l โŸง c else โŸฆ r โŸง c elim-sem (ยฌ P) l r c โ‰กโŸจโŸฉ (if not (eval P c) then โŸฆ l โŸง c else โŸฆ r โŸง c) - โ‰กโŸจ if-flip (eval P c) _ _ โŸฉ + โ‰กโŸจ if-not (eval P c) โŸฉ (if eval P c then โŸฆ r โŸง c else โŸฆ l โŸง c) โ‰กโŸจโŸฉ elim-sem P r l c @@ -70,11 +70,11 @@ elim-sem P l r c = if eval P c then โŸฆ l โŸง c else โŸฆ r โŸง c elim-sem (P โˆง Q) l r c โ‰กโŸจโŸฉ (if eval P c and eval Q c then โŸฆ l โŸง c else โŸฆ r โŸง c) - โ‰กโŸจ if-โˆง (eval P c) (eval Q c) _ _ โŸฉ + โ‰กโŸจ if-โˆง (eval P c) โŸฉ (if eval P c then (if eval Q c then โŸฆ l โŸง c else โŸฆ r โŸง c) else โŸฆ r โŸง c) โ‰กโŸจโŸฉ (if eval P c then elim-sem Q l r c else โŸฆ r โŸง c) - โ‰กโŸจ if-congหก (eval P c) (โ†“-presสณ Q l r c) โŸฉ + โ‰กโŸจ if-cong-then (eval P c) (โ†“-presสณ Q l r c) โŸฉ (if eval P c then โŸฆ โ†“ Q โŸจ l , r โŸฉ โŸง c else โŸฆ r โŸง c) โ‰กโŸจโŸฉ elim-sem P (โ†“ Q โŸจ l , r โŸฉ) r c @@ -85,7 +85,7 @@ elim-sem P l r c = if eval P c then โŸฆ l โŸง c else โŸฆ r โŸง c mutual โ†“-presหก : โˆ€ {A} (P : Prop F) (l r : ADT (Prop F) A) โ†’ โŸฆ P โŸจ l , r โŸฉ โŸงโ‚š โ‰— elim-sem P (elim-formulas l) (elim-formulas r) - โ†“-presหก P l r c = if-cong _ (preserves l c) (preserves r c) + โ†“-presหก P l r c = if-congโ‚‚ _ (preserves l c) (preserves r c) preserves : โˆ€ {A} @@ -120,7 +120,7 @@ lift (D โŸจ l , r โŸฉ) = var D โŸจ lift l , lift r โŸฉ lift-preserves : โˆ€ {A} โ†’ (e : ADT F A) โ†’ โŸฆ e โŸง โ‰— โŸฆ lift e โŸงโ‚š lift-preserves (leaf x) c = refl -lift-preserves (D โŸจ l , r โŸฉ) c = if-cong (c D) (lift-preserves l c) (lift-preserves r c) +lift-preserves (D โŸจ l , r โŸฉ) c = if-congโ‚‚ (c D) (lift-preserves l c) (lift-preserves r c) lift-compiler : LanguageCompiler (ADTL F) PropADTL lift-compiler = record diff --git a/src/Vatras/Translation/Lang/ADT/Rename.agda b/src/Vatras/Translation/Lang/ADT/Rename.agda index 04dbd854..829923b8 100644 --- a/src/Vatras/Translation/Lang/ADT/Rename.agda +++ b/src/Vatras/Translation/Lang/ADT/Rename.agda @@ -56,7 +56,7 @@ preserves-โŠ† f (d โŸจ l , r โŸฉ) config = ADT.โŸฆ f d โŸจ rename f l , rename f r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config (f d) then ADT.โŸฆ rename f l โŸง config else ADT.โŸฆ rename f r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config (f d) then_else_) (preserves-โŠ† f l config) (preserves-โŠ† f r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ† f l config) (preserves-โŠ† f r config) โŸฉ (if config (f d) then ADT.โŸฆ l โŸง (config โˆ˜ f) else ADT.โŸฆ r โŸง (config โˆ˜ f)) โ‰กโŸจโŸฉ ADT.โŸฆ d โŸจ l , r โŸฉ โŸง (config โˆ˜ f) @@ -73,9 +73,9 @@ preserves-โŠ‡ f fโปยน is-inverse (d โŸจ l , r โŸฉ) config = ADT.โŸฆ d โŸจ l , r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config d then ADT.โŸฆ l โŸง config else ADT.โŸฆ r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if config d then_else_) (preserves-โŠ‡ f fโปยน is-inverse l config) (preserves-โŠ‡ f fโปยน is-inverse r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ‡ f fโปยน is-inverse l config) (preserves-โŠ‡ f fโปยน is-inverse r config) โŸฉ (if config d then ADT.โŸฆ rename f l โŸง (config โˆ˜ fโปยน) else ADT.โŸฆ rename f r โŸง (config โˆ˜ fโปยน)) - โ‰กโŸจ Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (ADT.โŸฆ rename f l โŸง (config โˆ˜ fโปยน))) (ADT.โŸฆ rename f r โŸง (config โˆ˜ fโปยน)) โŸจ + โ‰กโŸจ Bool.if-cong (Eq.cong config (is-inverse d)) โŸจ (if config (fโปยน (f d)) then ADT.โŸฆ rename f l โŸง (config โˆ˜ fโปยน) else ADT.โŸฆ rename f r โŸง (config โˆ˜ fโปยน)) โ‰กโŸจโŸฉ ADT.โŸฆ f d โŸจ rename f l , rename f r โŸฉ โŸง (config โˆ˜ fโปยน) diff --git a/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda b/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda index 6a0d77a3..8c953449 100644 --- a/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda +++ b/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda @@ -14,6 +14,7 @@ module Vatras.Translation.Lang.ADT.WalkSemantics where open import Data.Bool using (Bool; true; false; not; if_then_else_) +open import Data.Bool.Properties using (if-cong) open import Data.Empty using (โŠฅ-elim) open import Data.List using (List; []; _โˆท_) open import Data.List.Relation.Unary.Any using (Any; here; there) @@ -169,7 +170,7 @@ path-to-fun-step-l-inner D l r lp (D' โŸจ a , b โŸฉ) ((.D' โ†ฃ .true) โˆท ep) tl โŸฆ D' โŸจ a , b โŸฉ โŸง c-big โ‰กโŸจโŸฉ (if c-big D' then โŸฆ a โŸง c-big else โŸฆ b โŸง c-big) - โ‰กโŸจ Eq.cong (if_then โŸฆ a โŸง c-big else โŸฆ b โŸง c-big) (path-to-fun-step-l-inner2 D l r lp tlp x D' (endswith-Any sub (here (fromWitness refl)))) โŸฉ + โ‰กโŸจ if-cong (path-to-fun-step-l-inner2 D l r lp tlp x D' (endswith-Any sub (here (fromWitness refl)))) โŸฉ (if c-sml D' then โŸฆ a โŸง c-big else โŸฆ b โŸง c-big) โ‰กโŸจ lem โŸฉ (if c-sml D' then โŸฆ a โŸง c-sml else โŸฆ b โŸง c-sml) diff --git a/src/Vatras/Translation/Lang/FST-to-OC.lagda.md b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md index 9a960eba..6a7f30ba 100644 --- a/src/Vatras/Translation/Lang/FST-to-OC.lagda.md +++ b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md @@ -278,17 +278,15 @@ induction (e@(_ โฒ _ โณ) โˆท cs) cโ‚ cโ‚‚ cโ‚ƒ pโ‚ pโ‚‚ pโ‚ƒ | just _ | jus induction (e@(_ โฒ _ โณ) โˆท cs) cโ‚ cโ‚‚ cโ‚ƒ pโ‚ pโ‚‚ pโ‚ƒ | just _ | just _ | nothing | _ with OC.โŸฆ cs โŸงโ‚’-recurse (cโ‚ โˆง cโ‚‚) in โŸฆcsโŸงcโ‚โˆงcโ‚‚ | OC.โŸฆ cs โŸงโ‚’-recurse cโ‚ | subtreeโ‚’-recurse cs (cโ‚ โˆง cโ‚‚) cโ‚ implies-โˆงโ‚ induction (e@(_ โฒ _ โณ) โˆท cs) cโ‚ cโ‚‚ cโ‚ƒ pโ‚ pโ‚‚ pโ‚ƒ | just _ | just _ | nothing | _ | .[] | .[] | [] = injโ‚‚ ( 0 -< [] >- โˆท [] - โ‰กโŸจ Eq.congโ‚‚ _โˆท_ refl โŸฆcsโŸงcโ‚โˆงcโ‚‚ โŸจ - 0 -< [] >- โˆท OC.โŸฆ cs โŸงโ‚’-recurse (cโ‚ โˆง cโ‚‚) โ‰กโŸจโŸฉ - catMaybes (just (0 -< [] >-) โˆท List.map (flip OC.โŸฆ_โŸงโ‚’ (cโ‚ โˆง cโ‚‚)) cs) - โ‰กโŸจ Eq.cong catMaybes (Eq.congโ‚‚ _โˆท_ (shared-artifact e cโ‚ cโ‚‚ - (Eq.trans (Eq.cong just (List.โˆท-injectiveหก pโ‚)) (Eq.sym โŸฆeโŸงcโ‚)) - (Eq.trans (Eq.cong just (List.โˆท-injectiveหก pโ‚‚)) (Eq.sym โŸฆeโŸงcโ‚‚))) - refl) โŸฉ - catMaybes (OC.โŸฆ e โŸงโ‚’ (cโ‚ โˆง cโ‚‚) โˆท List.map (flip OC.โŸฆ_โŸงโ‚’ (cโ‚ โˆง cโ‚‚)) cs) + catMaybes (just (0 -< [] >-) โˆท []) + โ‰กโŸจ Eq.cong (ฮป eq โ†’ catMaybes (eq โˆท [])) + (shared-artifact e cโ‚ cโ‚‚ + (Eq.trans (Eq.cong just (List.โˆท-injectiveหก pโ‚)) (Eq.sym โŸฆeโŸงcโ‚)) + (Eq.trans (Eq.cong just (List.โˆท-injectiveหก pโ‚‚)) (Eq.sym โŸฆeโŸงcโ‚‚))) โŸฉ + catMaybes (OC.โŸฆ e โŸงโ‚’ (cโ‚ โˆง cโ‚‚) โˆท []) โ‰กโŸจโŸฉ - OC.โŸฆ e โˆท cs โŸงโ‚’-recurse (cโ‚ โˆง cโ‚‚) + OC.โŸฆ e โˆท [] โŸงโ‚’-recurse (cโ‚ โˆง cโ‚‚) โˆŽ) ``` diff --git a/src/Vatras/Translation/Lang/NCC-to-2CC.agda b/src/Vatras/Translation/Lang/NCC-to-2CC.agda index 579bf9ed..d9cbe8fb 100644 --- a/src/Vatras/Translation/Lang/NCC-to-2CC.agda +++ b/src/Vatras/Translation/Lang/NCC-to-2CC.agda @@ -7,6 +7,7 @@ module Vatras.Translation.Lang.NCC-to-2CC where open import Size using (Size; โˆž) open import Data.Bool using (true; false; if_then_else_) +import Data.Bool.Properties as Bool import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin; zero; suc) open import Data.List as List using (List) @@ -70,7 +71,7 @@ module 2Ary where 2CC.โŸฆ d โŸจ translate l , translate r โŸฉ โŸง config โ‰กโŸจโŸฉ (if config d then 2CC.โŸฆ translate l โŸง config else 2CC.โŸฆ translate r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if_then_else_ (config d)) (preserves-โŠ† l config) (preserves-โŠ† r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ† l config) (preserves-โŠ† r config) โŸฉ (if config d then NCC.โŸฆ l โŸง (fnoc config) else NCC.โŸฆ r โŸง (fnoc config)) โ‰กโŸจ lemma โŸฉ Vec.lookup (NCC.โŸฆ l โŸง (fnoc config) โˆท NCC.โŸฆ r โŸง (fnoc config) โˆท []) (fnoc config d) @@ -109,7 +110,7 @@ module 2Ary where Vec.lookup (NCC.โŸฆ l โŸง config โˆท NCC.โŸฆ r โŸง config โˆท []) (config d) โ‰กโŸจ lemma โŸฉ (if conf config d then NCC.โŸฆ l โŸง config else NCC.โŸฆ r โŸง config) - โ‰กโŸจ Eq.congโ‚‚ (if_then_else_ (conf config d)) (preserves-โŠ‡ l config) (preserves-โŠ‡ r config) โŸฉ + โ‰กโŸจ Bool.if-congโ‚‚ _ (preserves-โŠ‡ l config) (preserves-โŠ‡ r config) โŸฉ (if conf config d then 2CC.โŸฆ translate l โŸง (conf config) else 2CC.โŸฆ translate r โŸง (conf config)) โ‰กโŸจโŸฉ 2CC.โŸฆ translate (d โŸจ l โˆท r โˆท [] โŸฉ) โŸง (conf config) diff --git a/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md b/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md index 5287217e..54efcf83 100644 --- a/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md +++ b/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md @@ -397,7 +397,7 @@ preservesโ‚’ c (T-artifact {a = a} {b = b} {ls = ls} {es = es} {rs = rs} {eโ‚ = preservesโ‚’ c (T-option {a = a} {O = O} {e = e} {ls = ls} {rs = rs} {eแต’โปสธ = ey} {eแต’โปโฟ = en} โŸถey โŸถen) with c O ... | true = begin Artifactแตฅ a (map (flip โŸฆ_โŸงโ‚‚ c) ls ++ (catMaybes (โŸฆ e โŸงโ‚’ c โˆท map (flip โŸฆ_โŸงโ‚’ c) (toList rs)))) - โ‰กโŸจ preservesโ‚’-option-size e โŸฉ -- prove that size constraint on e does not matter for โŸฆ_โŸงโ‚’ + โ‰กโŸจ preservesโ‚’-option-size {rs = rs} e โŸฉ -- prove that size constraint on e does not matter for โŸฆ_โŸงโ‚’ โŸฆ a -< ls โ‰ช e โˆท rs >- โŸงโ‚œ c โ‰กโŸจ preservesโ‚’ c โŸถey โŸฉ -- apply induction hypothesis โŸฆ ey โŸงโ‚‚ c diff --git a/src/Vatras/Translation/Lang/VT/Rename.agda b/src/Vatras/Translation/Lang/VT/Rename.agda index 0b6e491e..0bf591ab 100644 --- a/src/Vatras/Translation/Lang/VT/Rename.agda +++ b/src/Vatras/Translation/Lang/VT/Rename.agda @@ -11,12 +11,12 @@ variants. module Vatras.Translation.Lang.VT.Rename where open import Data.Bool using (if_then_else_) +open import Data.Bool.Properties using (if-cong; if-cong-then; if-congโ‚‚) open import Data.List as List using (List; []; _โˆท_; _++_) open import Data.Product using (_,_) open import Function using (id; _โˆ˜_) open import Relation.Binary.PropositionalEquality as Eq using (refl; _โ‰—_) -open import Vatras.Util.AuxProofs using (if-congหก; if-cong) open import Vatras.Data.EqIndexedSet using (_โ‰…[_][_]_; _โŠ†[_]_; โ‰…[]-sym) open import Vatras.Framework.Compiler using (LanguageCompiler) open import Vatras.Framework.Definitions using (๐”ธ; ๐”ฝ) @@ -79,9 +79,9 @@ module _ {Dโ‚ Dโ‚‚ : ๐”ฝ} {A : ๐”ธ} (f : Dโ‚ โ†’ Dโ‚‚) where VT.configure (rename' f (if[ p ]then[ l ])) config โ‰กโŸจโŸฉ (if Prop.eval (Prop.rename f p) config then VT.configure-all (rename'-all f l) config else []) - โ‰กโŸจ Eq.cong (if_then _ else []) (Prop.rename-spec f p config) โŸฉ + โ‰กโŸจ if-cong (Prop.rename-spec f p config) โŸฉ (if Prop.eval p (config โˆ˜ f) then VT.configure-all (rename'-all f l) config else []) - โ‰กโŸจ if-congหก (Prop.eval p (config โˆ˜ f)) (preserves-โŠ†-all l config) โŸฉ + โ‰กโŸจ if-cong-then (Prop.eval p (config โˆ˜ f)) (preserves-โŠ†-all l config) โŸฉ (if Prop.eval p (config โˆ˜ f) then VT.configure-all l (config โˆ˜ f) else []) โ‰กโŸจโŸฉ VT.configure (if[ p ]then[ l ]) (config โˆ˜ f) @@ -90,9 +90,9 @@ module _ {Dโ‚ Dโ‚‚ : ๐”ฝ} {A : ๐”ธ} (f : Dโ‚ โ†’ Dโ‚‚) where VT.configure (rename' f (if[ p ]then[ l ]else[ r ])) config โ‰กโŸจโŸฉ (if Prop.eval (Prop.rename f p) config then VT.configure-all (rename'-all f l) config else VT.configure-all (rename'-all f r) config) - โ‰กโŸจ Eq.cong (if_then _ else _) (Prop.rename-spec f p config) โŸฉ + โ‰กโŸจ if-cong (Prop.rename-spec f p config) โŸฉ (if Prop.eval p (config โˆ˜ f) then VT.configure-all (rename'-all f l) config else VT.configure-all (rename'-all f r) config) - โ‰กโŸจ if-cong _ (preserves-โŠ†-all l config) (preserves-โŠ†-all r config) โŸฉ + โ‰กโŸจ if-congโ‚‚ _ (preserves-โŠ†-all l config) (preserves-โŠ†-all r config) โŸฉ (if Prop.eval p (config โˆ˜ f) then VT.configure-all l (config โˆ˜ f) else VT.configure-all r (config โˆ˜ f)) โ‰กโŸจโŸฉ VT.configure (if[ p ]then[ l ]else[ r ]) (config โˆ˜ f) @@ -121,9 +121,9 @@ module _ {Dโ‚ Dโ‚‚ : ๐”ฝ} {A : ๐”ธ} (f : Dโ‚ โ†’ Dโ‚‚) (fโปยน : Dโ‚‚ โ†’ D VT.configure (if[ p ]then[ l ]) config โ‰กโŸจโŸฉ (if Prop.eval p config then VT.configure-all l config else []) - โ‰กโŸจ if-congหก (Prop.eval p config) (preserves-โŠ‡-all l config) โŸฉ + โ‰กโŸจ if-cong-then (Prop.eval p config) (preserves-โŠ‡-all l config) โŸฉ (if Prop.eval p config then VT.configure-all (rename'-all f l) (config โˆ˜ fโปยน) else []) - โ‰กโŸจ Eq.cong (if_then _ else []) (Prop.rename-preserves f fโปยน fโˆ˜fโปยนโ‰—id p config) โŸจ + โ‰กโŸจ if-cong (Prop.rename-preserves f fโปยน fโˆ˜fโปยนโ‰—id p config) โŸจ (if Prop.eval (Prop.rename f p) (config โˆ˜ fโปยน) then VT.configure-all (rename'-all f l) (config โˆ˜ fโปยน) else []) โ‰กโŸจโŸฉ VT.configure (rename' f (if[ p ]then[ l ])) (config โˆ˜ fโปยน) @@ -132,9 +132,9 @@ module _ {Dโ‚ Dโ‚‚ : ๐”ฝ} {A : ๐”ธ} (f : Dโ‚ โ†’ Dโ‚‚) (fโปยน : Dโ‚‚ โ†’ D VT.configure (if[ p ]then[ l ]else[ r ]) config โ‰กโŸจโŸฉ (if Prop.eval p config then VT.configure-all l config else VT.configure-all r config) - โ‰กโŸจ if-cong _ (preserves-โŠ‡-all l config) (preserves-โŠ‡-all r config) โŸฉ + โ‰กโŸจ if-congโ‚‚ _ (preserves-โŠ‡-all l config) (preserves-โŠ‡-all r config) โŸฉ (if Prop.eval p config then VT.configure-all (rename'-all f l) (config โˆ˜ fโปยน) else VT.configure-all (rename'-all f r) (config โˆ˜ fโปยน)) - โ‰กโŸจ Eq.cong (if_then _ else _) (Prop.rename-preserves f fโปยน fโˆ˜fโปยนโ‰—id p config) โŸจ + โ‰กโŸจ if-cong (Prop.rename-preserves f fโปยน fโˆ˜fโปยนโ‰—id p config) โŸจ (if Prop.eval (Prop.rename f p) (config โˆ˜ fโปยน) then VT.configure-all (rename'-all f l) (config โˆ˜ fโปยน) else VT.configure-all (rename'-all f r) (config โˆ˜ fโปยน)) โ‰กโŸจโŸฉ VT.configure (rename' f (if[ p ]then[ l ]else[ r ])) (config โˆ˜ fโปยน) diff --git a/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md b/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md index 8a5b3a98..6e99541c 100644 --- a/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md +++ b/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md @@ -18,7 +18,7 @@ module Vatras.Translation.Lang.VariantList-to-CCC open import Data.Nat using (โ„•; zero; suc) open import Data.List using ([]; _โˆท_; map) open import Data.List.NonEmpty using (Listโบ; _โˆท_) renaming (map to mapโบ) -open import Data.List.NonEmpty.Properties using () renaming (map-โˆ˜ to mapโบ-โˆ˜; map-cong to mapโบ-cong) +open import Data.List.NonEmpty.Properties using () renaming (map-id to mapโบ-id; map-โˆ˜ to mapโบ-โˆ˜; map-cong to mapโบ-cong) open import Data.Product using (_,_; projโ‚) open import Function using (id; flip; _โˆ˜_; _$_) @@ -34,7 +34,7 @@ open import Vatras.Lang.All.Fixed Dimension (Rose โˆž) open VariantList using (VariantList; VariantListL) open CCC using (CCC; CCCL; _โŸจ_โŸฉ) -open import Vatras.Util.List using (find-or-last; map-find-or-last; mapโบ-id) +open import Vatras.Util.List using (find-or-last; map-find-or-last) ``` ## Translation diff --git a/src/Vatras/Util/AuxProofs.agda b/src/Vatras/Util/AuxProofs.agda index 23090122..b803fefb 100644 --- a/src/Vatras/Util/AuxProofs.agda +++ b/src/Vatras/Util/AuxProofs.agda @@ -3,12 +3,9 @@ module Vatras.Util.AuxProofs where open import Level using (Level) open import Function using (id; _โˆ˜_) -open import Data.Bool using (Bool; false; true; if_then_else_; not; _โˆง_) -open import Data.Fin using (Fin; zero; suc; fromโ„•<) -open import Data.Nat using (โ„•; zero; suc; NonZero; _โ‰กแต‡_; _โŠ“_; _+_; _โˆธ_; _<_; _โ‰ค_; sโ‰คs; zโ‰คn) -open import Data.Nat.Properties using (n<1+n; mโŠ“nโ‰คm; +-comm; +-โˆธ-comm; nโˆธnโ‰ก0; mโ‰คn+m; +-โˆธ-assoc) -open import Data.Fin using (Fin; zero; suc; fromโ„•<) -open import Data.List.Properties using (length-++) +open import Data.Bool using (Bool; false; true) +open import Data.Nat using (โ„•; zero; suc; _โ‰กแต‡_; _+_; _โˆธ_; _<_; _โ‰ค_; sโ‰คs; zโ‰คn) +open import Data.Nat.Properties using (n<1+n; nโˆธnโ‰ก0; mโ‰คn+m) open import Data.Product using (_ร—_; _,_) open import Relation.Binary using (DecidableEquality) open import Relation.Nullary.Decidable using (yes; no) @@ -26,7 +23,6 @@ trueโ‰ขfalse : โˆ€ {a : Bool} trueโ‰ขfalse refl () ----- Some arithmetic properties --- TODO: Contribute some of these functions to STL โ‰กแต‡-refl : โˆ€ (n : โ„•) โ†’ (n โ‰กแต‡ n) โ‰ก true โ‰กแต‡-refl zero = refl @@ -43,69 +39,10 @@ n