Skip to content

Commit

Permalink
fix test
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Oct 30, 2024
1 parent 0cffb2a commit 19a2e28
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions test/MkIffOfInductive.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ example {α : Type _} (R : α → α → Prop) (a : α) (al : List α) :

-- check that the statement prints nicely
/--
info: test.chain_iff.{u_1} {α : Type u_1} (R : α → α → Prop) :
∀ (a : α) (a_1 : List α), List.Chain R a a_1a_1 = [] ∨ ∃ b l, R a b ∧ List.Chain R b l ∧ a_1 = b :: l
info: test.chain_iff.{u_1} {α : Type u_1} (R : α → α → Prop) (a✝ : α) (a✝¹ : List α) :
List.Chain R a✝ a✝¹a✝¹ = [] ∨ ∃ b l, R a b ∧ List.Chain R b l ∧ a✝¹ = b :: l
-/
#guard_msgs in
#check test.chain_iff
Expand Down

0 comments on commit 19a2e28

Please sign in to comment.