print command for a constructor of inductive predicate should print only the corresponding clause
When one uses print C
where C
is a constructor of an inductive definition, it should print
only the clause C
not the whole inductive definition.
When one uses print C
where C
is a constructor of an inductive definition, it should print
only the clause C
not the whole inductive definition.