Added refine for products and arrows

hazelgrove / hazel

Hazel, a live functional programming environment with typed holes

http://hazel.org/

MIT License

806 stars 52 forks source link

Added refine for products and arrows #1416

Open 7h3kk1d opened 3 weeks ago

7h3kk1d commented 3 weeks ago

Screencast from 2024-11-03 18-11-46.webm

Fills holes of the arrow type with an empty function and product type with an empty tuple. I'm neutral on name but @thomasporter522 had suggested refine since that's what agda uses.

cyrus- commented 3 weeks ago

let's call it Introduce instead of Refine
could also support single-constructor sum types

cyrus- commented 3 weeks ago

also add typfun for polymorphic functions

cyrus- commented 3 weeks ago

don't add extra parens in ap position