Я работал с Coq и столкнулся с некоторыми проблемами, пытаясь сопоставить объекты, созданные с помощью Axiom, с использованием подстановочного знака. Я создал минимальную программу Coq, которая демонстрирует мою проблему.
Inductive MyType : Set :=
| A
| B.
Definition MyFunction (n:MyType) : nat :=
match n with
| A => 0
| _ => 1
end.
Eval compute in MyFunction A.
Eval compute in MyFunction B.
Axiom C : MyType.
Eval compute in MyFunction C.
По сути, я требую, чтобы MyFunction C оценивалось как 1. Мне кажется, что Coq расширяет мой подстановочный знак _ до B, и это терпит неудачу, когда я пытаюсь применить функцию к этому бессмысленному объекту C. Я был бы признателен за совет о том, как это сделать Эта проблема.
