search

vaibhavkarve / igl2020

Lean project for Fall 2020
https://vaibhavkarve.github.io/igl2020/model
7 stars 2 forks source link

change inhabited to nonempty in lemma models_all_or_none_sentences #82

Closed vaibhavkarve closed 3 years ago

vaibhavkarve commented 3 years ago

This change was prompted by Lean's linter reporting that nonempty is preferred over inhabited. However, we were using the inhabited assumption in the proof since we referenced (arbitrary M.univ).

To fix the usage of arbitrary, we precede it with the tactic line inhabit M.univ. This converts nonempty into an inhabited assumption, and then the proof proceeds as before.