generics

generics copied to clipboard

Right now our encoding of telescopes is *overly dependent*. That is, any value in the telescope can appear in any of the types of the rest of the telescope. In...

flupe

What we claim in our paper is that it's fine to encode universe-polymorphic datatypes using our descriptions, as long as quantification over levels happen outside of the description. However, currently...

flupe

Everything.agda does not build (with standard library 1.7.1?)

4

Occurred during https://github.com/NixOS/nixpkgs/pull/153757. Build failure: ``` Checking Everything (/build/source/Everything.agda). Checking Generics.Prelude (/build/source/src/Generics/Prelude.agda). Checking Generics.Telescope (/build/source/src/Generics/Telescope.agda). Checking Generics.Telescope.Equality (/build/source/src/Generics/Telescope/Equality.agda). /build/source/src/Generics/Telescope/Equality.agda:26,13-14 Not in scope: J at /build/source/src/Generics/Telescope/Equality.agda:26,13-14 when scope checking J ```

turion

README.agda does not build (with standard library 1.7.1?)

1

I'm trying to build as part of https://github.com/NixOS/nixpkgs/pull/153757: ``` Checking README (/build/source/README.agda). Checking Generics.Prelude (/build/source/src/Generics/Prelude.agda). Checking Generics.Telescope (/build/source/src/Generics/Telescope.agda). Checking Generics.Desc (/build/source/src/Generics/Desc.agda). Checking Generics.HasDesc (/build/source/src/Generics/HasDesc.agda). Checking Generics.Accessibility (/build/source/src/Generics/Accessibility.agda). Checking Generics.All (/build/source/src/Generics/All.agda)....

turion

using this style of generic programming in other languages

2

Hello, i am idris2 programmer ( considering moving to lean 4 ) that wonders whether "Practical generic programming over a universe of native datatypes" can be applied to either of...

GunpowderGuy