ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-13 07:26:59 +03:00
Code Issues Projects Releases Wiki Activity
74fd10acf4
Idris-dev/test/proof010
History
Edwin Brady 13a36a3d32 Annotate functions as %hint for auto search 
This allows extra hints, as well as constructors, to guide proof search
for auto implicit arguments.
Added test proof010 which shows how this works to simulate type classes
with overlapping instances (and consequently no injectivity restriction
or assumption)

%hint only works on functions which return an instance of a data type.
Proof search exhaustively searches hints and constructors, so use with
care especially when adding lots of recursive or overlapping hints.
2015-03-29 21:24:04 +01:00
..
expected Annotate functions as %hint for auto search 2015-03-29 21:24:04 +01:00
proof010.idr Annotate functions as %hint for auto search 2015-03-29 21:24:04 +01:00
run Annotate functions as %hint for auto search 2015-03-29 21:24:04 +01:00