Commit 2021-05-20 19:10 32b433df
View on Github →refactor(*): remove some uses of omega in the library (#7620)
In #6129, we stopped using omega to avoid porting it to lean4.
Some new uses were added since then.
refactor(*): remove some uses of omega in the library (#7620)
In #6129, we stopped using omega to avoid porting it to lean4.
Some new uses were added since then.