]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/tests/test1.ma
checked in new version of matita from svn
[helm.git] / helm / matita / tests / test1.ma
1 set "baseuri" "cic:/matita/zack/aaa/".
2 inductive nat:Set \def O:nat | S:nat \to nat.
3 set "baseuri" "cic:/matita/zack/bbb/".
4 inductive nat:Set \def O:nat | S:nat \to nat.
5 alias id "nat" = "cic:/matita/zack/bbb/nat.ind#xpointer(1/1)".
6 inductive c:Set \def c1: nat \to c.