Scientific Computing in Lean

🖨

Miscellaneous

  1. Typeclasses as Interfaces and Function Overloading
    1. Function overloading
      1. Where is the Overloaded Function Defined?
        1. Finding the Definition Using #synth
        2. Alternative Method: Using pp.all
      2. Defining Functions "Inductively" on the Type
        1. Example: Summing Nested Structures
          1. Base Case: Natural Numbers
          2. Inductive Step: Lists
          3. Inductive Step: Products
          4. Handling More Complex Cases
        2. Working with Functions of Arbitrary Arity
        3. Exercise
        4. Polymorphism Over Types and Terms
        5. Exercises
    2. Typeclasses as Interfaces
      1. Defining an Array-like Interface
        1. Implementing the Interface
        2. Extending the Interface to Other Types
        3. Conclusion
  2. Working with Quotients
    1. Unordered Pair
    2. Symbolic Expressions
      1. Monoid Structure of ExprMonoid
        1. Example Usage