QpfTypes

QpfTypes copied to clipboard

In a regular `inductive` I can define arguments to a constructor by defining binders in front of the `:`. Currently, in `data` or `codata` this is not accepted: all arguments...

alexkeizer

The code is currently not very consistently formatted. It makes sense to follow Mathlib's style conventions, so we should go over the code and change it to be in line...

alexkeizer

Cleanup: get rid of noisy lines (e.g., `#check`)

1

We should use `#guard_msg` to assert, e.g., that a `#check` succeeds and gives the right type, without polluting the output of a build

alexkeizer

If a data type mentions a non-existent type, then rather than throwing an error, or even timing-out, the elaborator seems to get stuck in an infinite loop. ```lean data Foo...

alexkeizer

If a (co)inductive type does not involve quotients, then we don't need the full power of QPF's, PFunctors suffice. Polynomial functors have nicer def-eqs, so it would be nice if...

alexkeizer

feat: add DeepThunk

1

`DeepThunk` corresponds to the (co-)trace of a given polynomial functor, here we add the natural transformation required to generate them. These will later be used to inject into when generating...

Equilibris

Add the notion of a `DeepThunk` and generation for this

1

When it comes to expressing co-recursive functions, a state type is required to seed the progress. This state often also stores at what point the expression is in. This can...

Equilibris

Equilibris

alexkeizer

Currently, we implement `cases` using the recursor. This means every time we want to do a cases operation we have to walk the entire datastructure just to throw away the...

Equilibris