search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

A refine command which just suggests a refinement #608

Open UlfNorell opened 10 years ago

UlfNorell commented 10 years ago

From andreas....@gmail.com on April 06, 2012 11:40:12

Typically, when I refine a goal at function type, Agda puts variable names I do not like.

I'd prefer a refine which just fills a refinement suggestions into the hole, which I can then edit and then give to Agda.

Original issue: http://code.google.com/p/agda/issues/detail?id=608

UlfNorell commented 10 years ago

From nils.anders.danielsson on October 08, 2012 08:24:09

Status: Accepted
Labels: Priority-Low

UlfNorell commented 10 years ago

From andreas....@gmail.com on October 19, 2012 01:21:54

Labels: Interaction