feat(library/init/logic): add subsingleton.helim with heterogeneous equality
This commit is contained in:
parent
6c015a4954
commit
c646c3cacc
4 changed files with 9 additions and 0 deletions
|
@ -762,6 +762,9 @@ intro : (∀ a b : A, a = b) → subsingleton A
|
|||
protected definition subsingleton.elim {A : Type} [H : subsingleton A] : ∀(a b : A), a = b :=
|
||||
subsingleton.rec (λp, p) H
|
||||
|
||||
protected definition subsingleton.helim {A B : Type} [H : subsingleton A] (h : A = B) (a : A) (b : B) : a == b :=
|
||||
by induction h; apply heq_of_eq; apply subsingleton.elim
|
||||
|
||||
definition subsingleton_prop [instance] (p : Prop) : subsingleton p :=
|
||||
subsingleton.intro (λa b, !proof_irrel)
|
||||
|
||||
|
|
|
@ -195,6 +195,7 @@ name const * g_string_str = nullptr;
|
|||
name const * g_sub = nullptr;
|
||||
name const * g_subsingleton = nullptr;
|
||||
name const * g_subsingleton_elim = nullptr;
|
||||
name const * g_subsingleton_helim = nullptr;
|
||||
name const * g_tactic = nullptr;
|
||||
name const * g_tactic_all_goals = nullptr;
|
||||
name const * g_tactic_and_then = nullptr;
|
||||
|
@ -458,6 +459,7 @@ void initialize_constants() {
|
|||
g_sub = new name{"sub"};
|
||||
g_subsingleton = new name{"subsingleton"};
|
||||
g_subsingleton_elim = new name{"subsingleton", "elim"};
|
||||
g_subsingleton_helim = new name{"subsingleton", "helim"};
|
||||
g_tactic = new name{"tactic"};
|
||||
g_tactic_all_goals = new name{"tactic", "all_goals"};
|
||||
g_tactic_and_then = new name{"tactic", "and_then"};
|
||||
|
@ -722,6 +724,7 @@ void finalize_constants() {
|
|||
delete g_sub;
|
||||
delete g_subsingleton;
|
||||
delete g_subsingleton_elim;
|
||||
delete g_subsingleton_helim;
|
||||
delete g_tactic;
|
||||
delete g_tactic_all_goals;
|
||||
delete g_tactic_and_then;
|
||||
|
@ -985,6 +988,7 @@ name const & get_string_str_name() { return *g_string_str; }
|
|||
name const & get_sub_name() { return *g_sub; }
|
||||
name const & get_subsingleton_name() { return *g_subsingleton; }
|
||||
name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
|
||||
name const & get_subsingleton_helim_name() { return *g_subsingleton_helim; }
|
||||
name const & get_tactic_name() { return *g_tactic; }
|
||||
name const & get_tactic_all_goals_name() { return *g_tactic_all_goals; }
|
||||
name const & get_tactic_and_then_name() { return *g_tactic_and_then; }
|
||||
|
|
|
@ -197,6 +197,7 @@ name const & get_string_str_name();
|
|||
name const & get_sub_name();
|
||||
name const & get_subsingleton_name();
|
||||
name const & get_subsingleton_elim_name();
|
||||
name const & get_subsingleton_helim_name();
|
||||
name const & get_tactic_name();
|
||||
name const & get_tactic_all_goals_name();
|
||||
name const & get_tactic_and_then_name();
|
||||
|
|
|
@ -190,6 +190,7 @@ string.str
|
|||
sub
|
||||
subsingleton
|
||||
subsingleton.elim
|
||||
subsingleton.helim
|
||||
tactic
|
||||
tactic.all_goals
|
||||
tactic.and_then
|
||||
|
|
Loading…
Reference in a new issue