quantitative extensional type theory
rhiannon morris
d4cfbd4045
- `@[fail] def foo = ...` succeeds if `foo` has some error.
- `@[fail "scope"] def foo = ...` succeeds if `foo` has some error
containing the word "scope" somewhere
- `@[fail] namespace foo { }` works too and the error must be anywhere
in the namespace
|
||
|---|---|---|
| examples | ||
| exe | ||
| lib | ||
| tests | ||
| .gitignore | ||
| acsl.txt | ||
| CREDITS.md | ||
| pack.toml | ||
| qtuwu.png | ||
| quox.bib | ||
| README.md | ||
| syntax.ebnf | ||
quantitative extensional(ish) type theory
hey what would happen if some idiot tried to weld qtt and xtt together? let's find out together