small medium large xlarge

Back to: All Forums  PragPub
Generic-user-small
04 Apr 2013, 12:31
paul callaghan (14 posts)

IMPORTANT FIX

The final proof needs one more step. So instead of

Main.case_one_proof = proof { intro l; intro H; rewrite (sym H); trivial; }

You need this

Main.case_one_proof = proof { intro l; intro H; compute; rewrite (sym H); trivial; }

The extra “compute” is needed because Idris doesn’t (at present) simplify the goal before trying a rewrite step. (I’m used to proof assistants which do…)

Sorry about that!

You can see more discussion on this point at http://www.reddit.com/r/programming/comments/1bneoe/dependent_types_a_new_paradigm/c98aos8

Fernando_pragsmall
06 Sep 2017, 16:00
niusamip (1 post)

I have the same problem, hope someone will help here

You must be logged in to comment