feat(library/init/meta/vm): add decidable_eq for vm_obj_kind
This commit is contained in:
parent
8c50efeb75
commit
9b80e3bb62
1 changed files with 4 additions and 0 deletions
|
|
@ -5,6 +5,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import init.meta.tactic init.data.option.basic
|
||||
import init.meta.mk_dec_eq_instance
|
||||
|
||||
meta constant vm_obj : Type
|
||||
|
||||
|
|
@ -14,6 +15,9 @@ inductive vm_obj_kind
|
|||
| environment | tactic_state | format
|
||||
| options | other
|
||||
|
||||
instance vm_obj_kind_dec_eq : decidable_eq vm_obj_kind :=
|
||||
by tactic.mk_dec_eq_instance
|
||||
|
||||
namespace vm_obj
|
||||
meta constant kind : vm_obj → vm_obj_kind
|
||||
/- For simple and constructor vm_obj's, it returns the constructor tag/index.
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue