From a2ef6bd19eda5e674983376edcc443052ea1a863 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 20 Jul 2022 01:32:27 -0400 Subject: [PATCH] fix: malformed/misaligned markdown code fences --- src/Lean/Elab/Term.lean | 14 +++++++------- src/Lean/Meta/Match/Match.lean | 22 +++++++++++----------- tests/elabissues/issues8.lean | 1 + 3 files changed, 19 insertions(+), 18 deletions(-) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index ec0fda41a1..50c6eab784 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -850,13 +850,13 @@ Otherwise, we just use the basic `tryCoe`. Extensions for monads. -1- Try to unify `n` and `m`. If it succeeds, then we use - ``` - coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β - ``` - `n` must be a `Monad` to use this one. +1. Try to unify `n` and `m`. If it succeeds, then we use + ``` + coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β + ``` + `n` must be a `Monad` to use this one. -2- If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use +2. If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use ``` liftM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α ``` @@ -871,7 +871,7 @@ Extensions for monads. ``` -3- If there is a monad lif from `m` to `n` and a coercion from `α` to `β`, we use +3. If there is a monad lif from `m` to `n` and a coercion from `α` to `β`, we use ``` liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β ``` diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index b2ba02d2c8..c3f9aa9378 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -188,18 +188,18 @@ private def processAsPattern (p : Problem) : MetaM Problem := match alt.patterns with | Pattern.as fvarId p h :: ps => /- We used to use `checkAndReplaceFVarId` here, but `x` and `fvarId` may have different types - when dependent types are beind used. Let's consider the repro for issue #471 - ``` - inductive vec : Nat → Type - | nil : vec 0 - | cons : Int → vec n → vec n.succ + when dependent types are beind used. Let's consider the repro for issue #471 + ``` + inductive vec : Nat → Type + | nil : vec 0 + | cons : Int → vec n → vec n.succ - def vec_len : vec n → Nat - | vec.nil => 0 - | x@(vec.cons h t) => vec_len t + 1 + def vec_len : vec n → Nat + | vec.nil => 0 + | x@(vec.cons h t) => vec_len t + 1 - ``` - we reach the state + ``` + we reach the state ``` [Meta.Match.match] remaining variables: [x✝:(vec n✝)] alternatives: @@ -297,7 +297,7 @@ def assign (fvarId : FVarId) (v : Expr) : M Bool := do The first step is a variable-transition which replaces `β` with `β✝` in the first and third alternatives. The constraint `β✝ === α` in the second alternative is lost. Note that `α` is not an alternative variable. After applying the variable-transition step twice, we reach the following state - ``lean + ```lean [Meta.Match.match] remaining variables: [f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)] alternatives: [g:(Arrow α β✝)] |- [(Arrow.id .(β✝)), g] => h_1 β✝ g diff --git a/tests/elabissues/issues8.lean b/tests/elabissues/issues8.lean index fea4289061..73bd4e1930 100644 --- a/tests/elabissues/issues8.lean +++ b/tests/elabissues/issues8.lean @@ -7,6 +7,7 @@ The following example works, but it adds a coercion at `forceInt i`. The elaborated term is ``` fun (n i : Nat) => if n == i then forceNat n else forceInt (coe i) +``` -/ fun n i => if n == i then forceNat n else forceInt i -- works