diff --git a/lean/main/01_intro.lean b/lean/main/01_intro.lean index 7ee2679..3401465 100644 --- a/lean/main/01_intro.lean +++ b/lean/main/01_intro.lean @@ -128,8 +128,13 @@ elab "#assertType " termStx:term " : " typeStx:term : command => logInfo "success" catch | _ => throwError "failure" -#assertType 5 : Nat -- success -#assertType [] : Nat -- failure +/-- info: success -/ +#guard_msgs in --# +#assertType 5 : Nat + +/-- error: failure -/ +#guard_msgs in --# +#assertType [] : Nat /-! We started by using `elab` to define a `command` syntax. When parsed by the compiler, it will trigger the incoming computation. diff --git a/lean/main/05_syntax.lean b/lean/main/05_syntax.lean index 0543da0..d93868b 100644 --- a/lean/main/05_syntax.lean +++ b/lean/main/05_syntax.lean @@ -154,7 +154,7 @@ We can now write `MyTerm` in place of things like `1 + 1` and it will be it just means that the Lean parser can understand it: -/ -def Playground1.test := MyTerm +#check_failure MyTerm -- elaboration function for 'termMyTerm' has not been implemented -- MyTerm @@ -182,7 +182,7 @@ scoped syntax "⊥" : term -- ⊥ for false scoped syntax "⊤" : term -- ⊤ for true scoped syntax:40 term " OR " term : term scoped syntax:50 term " AND " term : term -#check ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes +#check_failure ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes end Playground2 @@ -203,9 +203,11 @@ syntax:50 boolean_expr " AND " boolean_expr : boolean_expr Now that we are working in our own syntax category, we are completely disconnected from the rest of the system. And these cannot be used in place of terms anymore: --/ +```lean #check ⊥ AND ⊤ -- expected term +``` +-/ /-! In order to integrate our syntax category into the rest of the system we will @@ -214,7 +216,7 @@ will re-embed it into the `term` category: -/ syntax "[Bool|" boolean_expr "]" : term -#check [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes +#check_failure [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes /-! ### Syntax combinators @@ -272,15 +274,17 @@ syntax binNumber := binDigit,+ /-! Since we can just use named parsers in place of syntax categories, we can now easily add this to the `term` category: --/ +```lean syntax "bin(" binNumber ")" : term #check bin(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes #check bin() -- fails to parse because `binNumber` is "one or many": expected 'O' or 'Z' +``` +-/ syntax binNumber' := binDigit,* -- note the * syntax "emptyBin(" binNumber' ")" : term -#check emptyBin() -- elaboration function hasn't been implemented but parsing passes +#check_failure emptyBin() -- elaboration function hasn't been implemented but parsing passes /-! Note that nothing is limiting us to only using one syntax combinator per parser, @@ -288,7 +292,7 @@ we could also have written all of this inline: -/ syntax "binCompact(" ("Z" <|> "O"),+ ")" : term -#check binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes +#check_failure binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes /-! As a final feature, let's add an optional string comment that explains the binary @@ -297,8 +301,8 @@ literal being declared: -- The (...)? syntax means that the part in parentheses is optional syntax "binDoc(" (str ";")? binNumber ")" : term -#check binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes -#check binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes +#check_failure binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes +#check_failure binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes /-! ## Operating on Syntax diff --git a/lean/main/06_macros.lean b/lean/main/06_macros.lean index 4af95e8..49c9d74 100644 --- a/lean/main/06_macros.lean +++ b/lean/main/06_macros.lean @@ -410,8 +410,8 @@ macro_rules -- in this case `error_position`, giving it the name `tk` | `(error_position%$tk first) => withRef tk (Macro.throwError "Ahhh") -#eval error_position all -- the error is indicated at `error_position all` -#eval error_position first -- the error is only indicated at `error_position` +#check_failure error_position all -- the error is indicated at `error_position all` +#check_failure error_position first -- the error is only indicated at `error_position` /- Obviously controlling the positions of errors in this way is quite important diff --git a/lean/main/07_elaboration.lean b/lean/main/07_elaboration.lean index c8d8328..23f597f 100644 --- a/lean/main/07_elaboration.lean +++ b/lean/main/07_elaboration.lean @@ -260,7 +260,7 @@ this information to complete elaboration. We can also easily provoke cases where this does not work out. For example: -/ -#check set_option trace.Elab.postpone true in List.foldr .add +#check_failure set_option trace.Elab.postpone true in List.foldr .add -- [Elab.postpone] .add : ?m.5808 → ?m.5809 → ?m.5809 -- invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant -- ?m.5808 → ?m.5809 → ?m.5809 @@ -328,9 +328,9 @@ def myanonImpl : TermElab := fun stx typ? => do elabTerm stx typ -- call term elaboration recursively #check (⟨⟨1, sorry⟩⟩ : Fin 12) -- { val := 1, isLt := (_ : 1 < 12) } : Fin 12 -#check ⟨⟨1, sorry⟩⟩ -- expected type must be known -#check (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor -#check (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat +#check_failure ⟨⟨1, sorry⟩⟩ -- expected type must be known +#check_failure (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor +#check_failure (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat /-! As a final note, we can shorten the postponing act by using an additional diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean index 208c009..2b683c2 100644 --- a/lean/main/09_tactics.lean +++ b/lean/main/09_tactics.lean @@ -39,9 +39,10 @@ We start by simply declaring the tactic with no implementation: syntax "custom_tactic" : tactic +/-- error: tactic 'tacticCustom_tactic' has not been implemented -/ +#guard_msgs in --# example : 42 = 42 := by custom_tactic --- tactic 'tacticCustom_tactic' has not been implemented sorry /- @@ -60,11 +61,13 @@ example : 42 = 42 := by We can now try a harder problem, that cannot be immediately dispatched by `rfl`: -/ -example : 43 = 43 ∧ 42 = 42:= by - custom_tactic --- tactic 'rfl' failed, equality expected --- 43 = 43 ∧ 42 = 42 --- ⊢ 43 = 43 ∧ 42 = 42 +#check_failure (by custom_tactic : 42 = 43 ∧ 42 = 42) +-- type mismatch +-- Iff.rfl +-- has type +-- ?m.1437 ↔ ?m.1437 : Prop +-- but is expected to have type +-- 42 = 43 ∧ 42 = 42 : Prop /- We extend the `custom_tactic` tactic with a tactic that tries to break `And` @@ -142,6 +145,7 @@ elab "custom_sorry_0" : tactic => do example : 1 = 2 := by custom_sorry_0 -- unsolved goals: ⊢ 1 = 2 + sorry /- This defines a syntax extension to Lean, where we are naming the piece of syntax @@ -172,6 +176,7 @@ example : 1 = 2 := by custom_sorry_1 -- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) -- unsolved goals: ⊢ 1 = 2 + sorry /- To `sorry` the goal, we can use the helper `Lean.Elab.admitGoal`: @@ -242,6 +247,7 @@ example (H1 : 1 = 1) (H2 : 2 = 2): 2 = 2 := by -- H1 : 1 = 1 -- H2 : 2 = 2 -- ⊢ 2 = 2 + sorry example (H1 : 1 = 1): 2 = 2 := by custom_assump_0 @@ -249,6 +255,7 @@ example (H1 : 1 = 1): 2 = 2 := by -- unsolved goals -- H1 : 1 = 1 -- ⊢ 2 = 2 + sorry /- Next, we access the list of hypotheses, which are stored in a data structure @@ -387,8 +394,7 @@ elab "custom_assump_2" : tactic => example (H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by custom_assump_2 -example (H1 : 1 = 1): 2 = 2 := by - custom_assump_2 +#check_failure (by custom_assump_2 : (H1 : 1 = 1) → 2 = 2) -- tactic 'custom_assump_2' failed, unable to find matching hypothesis of type (2 = 2) -- H1 : 1 = 1 -- ⊢ 2 = 2 @@ -466,6 +472,7 @@ theorem test_reverse_goals : (1 = 2 ∧ 3 = 4) ∧ 5 = 6 := by -- ⊢ 3 = 4 -- case left.left -- ⊢ 1 = 2 + all_goals sorry /- ## FAQ @@ -571,16 +578,11 @@ elab "faq_throw_error" : tactic => let goal ← Lean.Elab.Tactic.getMainGoal Lean.Meta.throwTacticEx `faq_throw_error goal "throwing an error at the current goal" -example (b : Bool): b = true := by - cases b; - faq_throw_error - -- case true - -- ⊢ true = true - -- tactic 'faq_throw_error' failed, throwing an error at the current goal - -- case false - -- ⊢ false = true +#check_failure (by faq_throw_error : (b : Bool) → b = true) +-- tactic 'faq_throw_error' failed, throwing an error at the current goal +-- ⊢ ∀ (b : Bool), b = true -/- +/-! **Q: What is the difference between `Lean.Elab.Tactic.*` and `Lean.Meta.Tactic.*`?** A: `Lean.Meta.Tactic.*` contains low level code that uses the `Meta` monad to