operatorsmade with verso-snippets
View
-- The result type is computed from the operands (an `outParam`), so no annotation
-- is ever needed in generated code:
example : Int    := (1 : Int) +ₚ (2 : Int)
example : Rat    := (1 : Int) +ₚ (2.5 : Rat)
example : String := "pas" +ₚ "ta"

-- Python's `+` on lists concatenates. Mathlib's `Add (List α)` adds POINTWISE,
-- so without a higher-priority instance this would quietly be [4, 6]:
#eval ([1, 2] : List Int) +ₚ ([3, 4] : List Int)

[1, 2, 3, 4]-- Python floors; Lean's own `Int` division truncates. Python is the specification:
#eval pyFloorDiv (7 : Int) (-2 : Int)   -- -4, not -3
-4#eval pyMod      (7 : Int) (-2 : Int)   -- -1, not 1

-1-- and each operator ships a lemma rewriting it back to Lean's arithmetic, by `rfl`,
-- which is what lets `ring` and `omega` finish a goal about generated code:
example (a b : Int) : a +ₚ b = a + b := bya:ℤb:ℤ⊢ a +ₚ b = a + b rflAll goals completed! 🐙