お腹空いた...
#include <iostream> using namespace std; struct True{}; struct False{}; struct Zero{}; template<typename T> struct Succ{}; template<typename A,typename B> struct Add { }; template<typename B> struct Add<Zero,B> { typedef B val; }; template<typename A,typename B> struct Add<Succ<A>,B> { typedef typename Add<A,B>::val ret; typedef Succ<ret> val; }; template<typename V1,typename V2> struct NatEq{}; template<> struct NatEq<Zero,Zero> { typedef True val; }; template<typename A> struct NatEq<Succ<A>,Succ<A>> { typedef True val; }; template<typename T1,typename T2> struct Eq{}; template<typename T> struct Eq<T,T>{typedef True val;}; template<typename T> struct succEq { }; template<typename V> struct succEq<Eq<V,V> > { typedef Eq<Succ<V>,Succ<V> > val; }; template<typename T> struct lem1 { }; template<> struct lem1<Zero> { typedef Eq<Add<Zero,Zero>::val,Add<Zero,Zero>::val> proofed; }; template<typename A> struct lem1<Succ<A> > { typedef typename lem1<A>::proofed hypo; typedef typename succEq<hypo>::val proofed; }; int main() { typedef Succ<Succ<Succ<Zero>>> Three; typedef lem1<Three>::proofed::val test; }
要は a + 0 = 0 + aだよねっていう可換の特殊な場合についての証明・・・のつもりなんですが結局値を投げ込まないとコンパイル時にどうこうしてくれないのでうーん・・・？？
