@@ -107,17 +107,17 @@ def ctorSuggestion1 (pair : MyProd) : Nat :=
107107/--
108108error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`
109109
110- Hint: These are similar :
111- 'Lean.Grind.AC.Seq. cons',
112- 'List.Lex.below. cons',
113- ' List.Lex.cons',
114- ' List.Pairwise .below.cons',
115- ' List.Pairwise. cons',
116- ' List.Perm .below.cons',
117- ' List.Perm. cons',
118- ' List.Sublist.below.cons',
119- ' List.Sublist .cons',
120- ' List.cons'
110+ Hint: Using one of these would be valid :
111+ [ apply ] `List.Sublist. cons`
112+ [ apply ] `Lean.Grind.AC.Seq. cons`
113+ [ apply ] ` List.Lex.cons`
114+ [ apply ] ` List.Perm .below.cons`
115+ [ apply ] ` List.Lex.below. cons`
116+ [ apply ] ` List.Pairwise .below.cons`
117+ [ apply ] ` List.cons`
118+ [ apply ] ` List.Sublist.below.cons`
119+ [ apply ] ` List.Perm .cons`
120+ [ apply ] ` List.Pairwise. cons`
121121---
122122warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
123123
@@ -137,18 +137,18 @@ inductive StringList : Type where
137137/--
138138error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`
139139
140- Hint: These are similar :
141- 'Lean.Grind.AC.Seq. cons',
142- 'List.Lex.below. cons',
143- ' List.Lex.cons',
144- ' List.Pairwise .below.cons',
145- ' List.Pairwise. cons',
146- ' List.Perm .below.cons',
147- ' List.Perm. cons',
148- ' List.Sublist.below.cons',
149- ' List.Sublist .cons',
150- ' List.cons',
151- (or 1 others)
140+ Hint: Using one of these would be valid :
141+ [ apply ] `List.Sublist. cons`
142+ [ apply ] `Lean.Grind.AC.Seq. cons`
143+ [ apply ] ` List.Lex.cons`
144+ [ apply ] ` List.Perm .below.cons`
145+ [ apply ] ` List.Lex.below. cons`
146+ [ apply ] ` List.Pairwise .below.cons`
147+ [ apply ] ` List.cons`
148+ [ apply ] ` List.Sublist.below.cons`
149+ [ apply ] ` List.Perm .cons`
150+ [ apply ] ` List.Pairwise. cons`
151+ [ apply ] `StringList.cons`
152152---
153153warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
154154
0 commit comments