Skip to content

Commit

Permalink
Remove test commands
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman committed Dec 10, 2024
1 parent a5b627c commit a30534d
Showing 1 changed file with 0 additions and 5 deletions.
5 changes: 0 additions & 5 deletions lean/Raylean/Graphics2D/Image.lean
Original file line number Diff line number Diff line change
Expand Up @@ -188,11 +188,6 @@ theorem image_comp_map (g : α → β) (h : β → γ) (x : Image α):
guard_target = (fun l => (h ∘ g) (x l)) = fun l => h (g (x l))
simp

-- #find [] ++ ?x = ?x
-- #loogle [] ++ ?x = ?x

#help tactic

instance : LawfulFunctor Image where
map_const := image_map_const
id_map := image_id_map
Expand Down

0 comments on commit a30534d

Please sign in to comment.