Commit 2023-03-18 15:37 f5297896

View on Github →

feat: port Data.Dfinsupp.WellFounded (#2944) Other changes:

  • modify Data/Dfinsupp/Lex to use explicit (i : ι);
  • fix 2 typos&align in Logic.Basic.

Estimated changes

modified theorem Dfinsupp.lex_def
modified theorem Pi.lex_eq_dfinsupp_lex
added theorem Dfinsupp.Lex.acc
added theorem Dfinsupp.Lex.acc_zero
added theorem Dfinsupp.lex_fibration
added theorem Pi.Lex.wellFounded