Autoinduct, add more tests

coq-community / metaprogramming-rosetta-stone

A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]

MIT License

17 stars 5 forks source link

Autoinduct, add more tests #10

Open tlringer opened 1 year ago

tlringer commented 1 year ago

Some cases to test:

Function on both sides of equality
Multiple different fixpoints occur in goal
Function constant is an alias for another constant, which wraps the fixpoint
Under binders (ambitious)
Different numbers of arguments
Currying
Let

Probably more.

tlringer commented 1 year ago

Many are done, may add more later to test some of the remaining three cases mentioned here though (let, binders, currying)