Inductive eq {Ty : Set} : Ty -> Ty -> Set := | Refl : forall v , eq v v. Inductive sgl {Ty : Set} : Ty -> Set := | Sgl : forall v , sgl v. Definition test {ts ts' : nat} (obj : eq ts ts') (s : sgl ts) : sgl ts' := match obj with | Refl v =…

この間リナカフェでも話したお話なんですが #include <iostream> using namespace std; template<class T> struct id{ typedef T type; }; template<class T> void f(T t){ cout << "ue" << endl; } template<class T> void f(id<T>::type t){ cout << "shita" << endl; } int main() { f<int>(0); return </int></t></class></class></class></iostream>…

多分rvoっていう事で話は終わった。 #include <iostream> #include <typeinfo> #include <cxxabi.h> using namespace std; char* demangle(const char *demangle) { int status; return abi::__cxa_demangle(demangle, 0, 0, &status); } /* Sはあらゆる方法で生成出来ないようにしたい修造</cxxabi.h></typeinfo></iostream>…

最近"A Semantic Analysis of C++ Templates"という、「C++のテンプレートが未だにまともに、"自然言語じゃない形で"形式化されてないから俺らがやってやった！！」という論文を読みました。論文の在処 : http://ecee.colorado.edu/~siek/pubs/pubs/2006/sie…