Refinement of inductive type implemented.

[helm.git] / helm / software / matita / tests / ng_commands.ma

diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma
index 75d3eda6a78bff973519efcc4b0659d341f026df..03d9df0927824cfe6dce028b5bac37220268e29a 100644 (file)
--- a/helm/software/matita/tests/ng_commands.ma
+++ b/helm/software/matita/tests/ng_commands.ma
@@ -39,11 +39,9 @@ ntheorem nzero_ok: nzero (S (S O)) = O.
  napply (refl_eq ? O);
 nqed.
 
-(*
 ninductive nnat: Type ≝
    nO: nnat
  | nS: nnat → nnat.
-*)
 
 (* testare anche i record e le ricorsioni/coricorsioni/(co)induttivi MUTUI *)