API tools faq
paste
Advertisement
Guest User

trace.simp_lemmas output

a guest
Jan 11th, 2019
128
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 5.30 KB | None | 0 0
raw download clone embed print report
  1. invalid simplification lemma 'fol.subst_var_bounded_formula' (use command 'set_option trace.simp_lemmas true' for more details)
  2. state:
  3. ⊢ ∀'(&0 ∈' &1 ⟹ is_ordered_pair ↑' 1 # 1) = ∀'(&0 ∈' &1 ⟹ (is_ordered_pair ⊚ [0]))
  4.  
  5. [simp_lemmas.invalid] LHS of rule derived from 'dvd_refl' occurs in RHS
  6. [simp_lemmas.invalid] rule derived from 'one_dvd' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  7. [simp_lemmas.invalid] rule derived from 'dvd_mul_right' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  8. [simp_lemmas.invalid] rule derived from 'dvd_mul_left' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  9. [simp_lemmas.invalid] rule derived from 'list.nil_subset' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  10. [simp_lemmas.invalid] LHS of rule derived from 'list.subset.refl' occurs in RHS
  11. [simp_lemmas.invalid] rule derived from 'list.subset_cons' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  12. [simp_lemmas.invalid] rule derived from 'list.subset_append_left' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  13. [simp_lemmas.invalid] rule derived from 'list.subset_append_right' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  14. [simp_lemmas.invalid] rule derived from 'set.empty_subset' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  15. [simp_lemmas.invalid] rule derived from 'set.subset_union_left' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  16. [simp_lemmas.invalid] rule derived from 'set.subset_union_right' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  17. [simp_lemmas.invalid] rule derived from 'set.subset_insert' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  18. [simp_lemmas.invalid] rule derived from 'lattice.le_sup_left' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  19. [simp_lemmas.invalid] rule derived from 'lattice.le_sup_right' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  20. [simp_lemmas.invalid] rule derived from 'lattice.bot_le' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  21. [simp_lemmas.invalid] rule derived from 'zero_le' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  22. [simp_lemmas.invalid] rule derived from 'units.coe_dvd' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  23. [simp_lemmas.invalid] rule derived from 'list.nil_sublist' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  24. [simp_lemmas.invalid] LHS of rule derived from 'list.sublist.refl' occurs in RHS
  25. [simp_lemmas.invalid] rule derived from 'list.sublist_cons' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  26. [simp_lemmas.invalid] rule derived from 'list.sublist_append_left' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  27. [simp_lemmas.invalid] rule derived from 'list.sublist_append_right' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  28. [simp_lemmas.invalid] rule derived from 'list.prefix_append' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  29. [simp_lemmas.invalid] rule derived from 'list.suffix_append' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  30. [simp_lemmas.invalid] rule derived from 'list.infix_append' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  31. [simp_lemmas.invalid] rule derived from 'list.suffix_cons' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  32. [simp_lemmas.invalid] rule derived from 'list.prefix_concat' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  33. [simp_lemmas.invalid] rule derived from 'list.suffix_insert' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  34. [simp_lemmas.invalid] rule derived from 'nat.cast_nonneg' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  35. [simp_lemmas.invalid] LHS of rule derived from 'multiset.subset.refl' occurs in RHS
  36. [simp_lemmas.invalid] rule derived from 'multiset.zero_subset' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  37. [simp_lemmas.invalid] rule derived from 'multiset.le_ndinsert_self' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
  38. [simp_lemmas.invalid] LHS of rule derived from 'finset.subset.refl' occurs in RHS
  39. [simp_lemmas.invalid] rule derived from 'finset.empty_subset' contains argument that is (a) not a Prop, (b) not an instance, and (c) not in the LHS of the rule
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!