examples/Examples/InteractExample3g3kno8ekkpr.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. class Ex.Add line 2 source

   no axioms what this means

   Distinct definitions of this name: book/TPiL/TypeClasses.lean:23 (different declaration text), examples/Examples/InteractExamplextkkn9qu4li2b.lean:2 (different declaration text). Qualify references as Ex.Add@path.

2. instance Ex.(instance at line 5) line 5 source

   Source comment

   ----

   instance : Add Nat where
   …

3. instance Ex.(instance at line 8) line 8 source
4. instance Ex.(instance at line 11) line 11 source