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 | View the thread | More toots from BoydStephenSmithJr@hachyderm.io

Mentions

Tags

=> View idris tag