Coq: Сокращение определений индуктивных типов

Предположим, у меня есть индуктивный тип с конструкторами того же типа, например.

Inductive A := a (x:nat)(y:Set) | b (x:nat)(y:Set).

Можно ли сократить его определение, чтобы мне не пришлось повторять тип (возможно, параметризованный) для каждого конструктора, например. что-то типа

Inductive A := (a | b) (x:nat)(y:Set).

types syntax definition coq abbreviation
person jaam    schedule 12.05.2017    source источник
comment
YMMV, но в этом случае я бы сделал один конструктор с логическим флагом.   -  person ejgallego    schedule 13.05.2017
comment
@ejgallego: Хорошо ... и флаг nat, если конструкторов много?   -  person jaam    schedule 13.05.2017
comment
Вероятно, порядковый флаг 'I_k   -  person ejgallego    schedule 13.05.2017
comment
Имейте в виду, что вы можете взломать отображение с помощью нотаций, поэтому регистр true и false может отображаться (и анализироваться!) как другой индуктивный.   -  person ejgallego    schedule 13.05.2017
comment
@ejgallego: Где (или как) определяются ваши порядковые номера? (Моя идея состояла в том, чтобы использовать nat в частичной функции.)   -  person jaam    schedule 14.05.2017
comment
Существуют различные способы определения порядковых номеров, см., например, stackoverflow.com/questions/42871971/, но в SO есть и другие примеры.   -  person ejgallego    schedule 14.05.2017
comment
@ejgallego: единственная проблема с отображением значений флагов в виде разных обозначений заключается в том, что это будет больше кода, чем с разными конструкторами.   -  person jaam    schedule 19.05.2017