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
220f400ad4
Idris-dev/test/pruviloj001
History
David Raymond Christiansen c9973eb7c3 Add andThen and refine to Pruviloj 
andThen is a subgoal sequencing combinator, and refine is a bit like
Coq's eapply.
2015-10-01 18:28:40 +02:00
..
expected Library of tactics for proof automation with Elab 2015-09-25 13:24:42 +02:00
pruviloj001.idr Add andThen and refine to Pruviloj 2015-10-01 18:28:40 +02:00
run Library of tactics for proof automation with Elab 2015-09-25 13:24:42 +02:00