workflow for making lambdas and numeric literals

[ivoysey]

it's a little weird to create a lam. cause the action's greyed out even when it's ok until you supply the variable. so it kind of looks like it's not ok. and then you put a variable in the text box, and press the action key but that changes the variable name from x to x\. the hot key only works again after you click outside the box to remove focus

[cyrus-]

the intent is for \ to move you to the box to enter the variable name, and then enter does the action. so roughly following what you would do in e.g. Haskell -- type '\' then the variable then '.' or whatever

[ivoysey]

ah! that is smoother; I hadn't tripped across that particular pattern yet.

---Ian

On 10 October 2016 at 12:13, Cyrus Omar notifications@github.com wrote:

the intent is for \ to move you to the box to enter the variable name, and then enter does the action. so roughly following what you would do in e.g. Haskell -- type '\' then the variable then '.' or whatever

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/28#issuecomment-252668098, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIDXS1FfrxEFutWFB7wAgzIl3IOJcks5qymRBgaJpZM4KSsGc .

[MichaelHilton]

We could put in a "placeholder" string to try to make it easier for users. What do you think? There is probably a better string than "enter a value"

[cyrus-]

"(enter variable then press ENTER)" perhaps?

Also it might clarify matters + make it more consistent with the paper for the input boxes to be to the right of the buttons.

On Mon, Oct 10, 2016, 12:25 Michael Hilton notifications@github.com wrote:

We could put in a "placeholder" string to try to make it easier for users. What do you think? There is probably a better string than "enter a value" [image: screen shot 2016-10-10 at 9 24 00 am] https://cloud.githubusercontent.com/assets/1170420/19243167/53556140-8ecb-11e6-9861-e482f2499f34.png

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/28#issuecomment-252670829, or mute the thread https://github.com/notifications/unsubscribe-auth/AARIPuq_EJRfpCngCkfQgR0Zk-XEaUnOks5qymbigaJpZM4KSsGc .

[MichaelHilton]

I'll try that out and post a screen shot...

[MichaelHilton]

Better?

[cyrus-]

Should say variable not value. And the case button is still on the right.

On Mon, Oct 10, 2016, 12:32 Michael Hilton notifications@github.com wrote:

Better? [image: screen shot 2016-10-10 at 9 31 03 am] https://cloud.githubusercontent.com/assets/1170420/19243404/690e6c4c-8ecc-11e6-9153-ca66360072a3.png

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/28#issuecomment-252672629, or mute the thread https://github.com/notifications/unsubscribe-auth/AARIPmX-lu9kbzJ66kG2-0IzOGr9ZtV0ks5qymiTgaJpZM4KSsGc .

[MichaelHilton]

are you ok with "var"? it is getting kinda long

[cyrus-]

Sure that's fine.

On Mon, Oct 10, 2016, 12:34 Michael Hilton notifications@github.com wrote:

are you ok with "var"? it is getting kinda long

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/28#issuecomment-252673217, or mute the thread https://github.com/notifications/unsubscribe-auth/AARIPkpo6eI5Ltk16QmrH5OJ4li47AFPks5qymkkgaJpZM4KSsGc .

[MichaelHilton]

[cyrus-]

The construct lit one shouldn't say "var", that one is a "number". Other than that, looks good to me.

[ivoysey]

Looks good to me, too!

---Ian

On 10 October 2016 at 12:40, Cyrus Omar notifications@github.com wrote:

The construct lit one shouldn't say "var", that one is a "number". Other than that, looks good to me.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/28#issuecomment-252674645, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIClgtM-8e4GZ8P41OH_iFP-JmA66ks5qymqWgaJpZM4KSsGc .

[MichaelHilton]

I'm trying to come up with a way to have the button say "ap" like in the paper, but also say "application" so it is not too cryptic. Not sold on this.... What do you think?

[cyrus-]

nah I don't think that's necessary. If someone isn't sure what a button does, playing with it a bit should clarify that. I like leaving the buttons with the same text as the actions in the paper.

[cyrus-]

If you really want to add some explanation, maybe add a tooltip?

[ivoysey]

maybe italics for the part that's the syntax from the shapes, and then the full word for human readability? the caps jumps out a bit too much.

also, maybe [ . ] instead of ( . ) to show the hotkey on the buttons? i just realized that's what that was for; i'd been confused by (() on the ap button for a while but ignoring it.

---Ian

On 10 October 2016 at 12:42, Michael Hilton notifications@github.com wrote:

I'm trying to come up with a way to have the button say "ap" like in the paper, but also say "application" so it is not too cryptic. Not sold on this.... What do you think?

[image: screen shot 2016-10-10 at 9 40 57 am] https://cloud.githubusercontent.com/assets/1170420/19243736/b7408b42-8ecd-11e6-8091-3e4a79cd4491.png

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/28#issuecomment-252674977, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIMl8cPj4NUlYAa217nVvj01ZA8amks5qymrpgaJpZM4KSsGc .

[cyrus-]

agreed on using [ . ] instead of ( . )

[MichaelHilton]

sounds good

[cyrus-]

or use some other styling for the hotkey, e.g. bold or a different background box. I think buttons can have arbitrary HTML inside them

[MichaelHilton]

unfortunately, you can't style button labels with html...

[MichaelHilton]

I'm thinking of making the "hazelnut" text here a link to the paper. does that sound good? where should we link it to?

[cyrus-]

That looks good to me.

Link to ArXiV for now. We should update ArXiV with the version of the paper we submitted to AE. I'll make an issue for that.

[ivoysey]

possibly just hazelgrove.org when it's live? that should have links to the preprint and agda that are prominent.

---Ian

On 10 October 2016 at 12:55, Michael Hilton notifications@github.com wrote:

I'm thinking of making the "hazelnut" text here a link to the paper. does that sound good? where should we link it to? [image: screen shot 2016-10-10 at 9 54 02 am] https://cloud.githubusercontent.com/assets/1170420/19244068/7e69054a-8ecf-11e6-9601-9c002dcda010.png

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/28#issuecomment-252678057, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIHe64kFhTHgBGvarcUqWLyLIPtg0ks5qym3ogaJpZM4KSsGc .

[cyrus-]

Yeah maybe label the link at the bottom "Source (OCaml): " and add another "Mechanization (Agda): " link below that

[MichaelHilton]