Sébastien Michelland lephe
lephe
/ iterfold-gist.cc
Created
June 23, 2024 08:55
A C++20 range adaptor for generating the series of partial folds of range over a function.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /* http://silent-tower.net/projects/cpp-iterfold | |
| g++ iterfold-gist.cc -o iterfold-gist -O2 -Wall -Wextra -std=c++23 | |
| (generator and range adaptor closure require c++23, otherwise c++20 is fine) | |
| (generator requires g++/libstdc++ 14 at time of writing) */ | |
| #include <iterator> | |
| #include <functional> | |
| #include <ranges> | |
| /*** iterfold implementation ***/ |
lephe
/ ParameterizedMLIRTypes.lean
Created
May 6, 2022 16:25
Break the MLIR type/attribute dependency cycle by quantifying on a generic type, thus limiting by universes instead
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Lean | |
| section | |
| universe u | |
| -- TODO/Problem: does not enforce unique use of names | |
| structure MLIRTypeable (name: String) (α: Type u) where | |
| decEq: DecidableEq α | |
| axiom MLIRTypeable.unique (n₁ n₂: String): |