Ancestors

Toot

Written by Boyd Stephen Smith Jr. on 2024-11-18 at 03:39

Okay, tests are in place, and I think do pretty good coverage on the meat of the new #idris library.

However, before I request it be added to the package db, this needs some "work", I think:

record Lan {k : Type} (f : k -> Type) (g : k -> Type) a where
  constructor MkLan
  target : k
  extract : f target -> a
  pool : g target

I'm adapting left Kan-extensions from the Haskell library. I want names for the fields, but "target" should be implicit (and existential). How to do that?

=> More informations about this toot | More toots from BoydStephenSmithJr@hachyderm.io

Descendants

Written by Boyd Stephen Smith Jr. on 2024-11-18 at 03:57

If you'd rather discuss this on the Idris ... Discord (shudder), I created a post there: https://discord.com/channels/827106007712661524/1307917402754908160

=> More informations about this toot | More toots from BoydStephenSmithJr@hachyderm.io

Written by Boyd Stephen Smith Jr. on 2024-11-18 at 04:26

I did get an answer pretty quick on the discord server. I don't think it was in the documentation. But, problem solved, in any case.

Basically, implicit fields can just be bracketed.

I'm going to wait until tomorrow to implement it. So, no release before then.

=> More informations about this toot | More toots from BoydStephenSmithJr@hachyderm.io