chore: Version 0.3 #136
|
@ -264,25 +264,24 @@ def serializeName (name: Name) (sanitize: Bool := true): String :=
|
|||
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
|
||||
|
||||
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
|
||||
partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
|
||||
partial def serializeSortLevel (level: Level) : String :=
|
||||
let k := level.getOffset
|
||||
let u := level.getLevelOffset
|
||||
let u_str := match u with
|
||||
| .zero => "0"
|
||||
| .succ _ => panic! "getLevelOffset should not return .succ"
|
||||
| .max v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
let v := serializeSortLevel v
|
||||
let w := serializeSortLevel w
|
||||
s!"(:max {v} {w})"
|
||||
| .imax v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
let v := serializeSortLevel v
|
||||
let w := serializeSortLevel w
|
||||
s!"(:imax {v} {w})"
|
||||
| .param name =>
|
||||
let name := serializeName name sanitize
|
||||
s!"{name}"
|
||||
| .mvar id =>
|
||||
let name := serializeName id.name sanitize
|
||||
let name := id.name
|
||||
s!"(:mv {name})"
|
||||
match k, u with
|
||||
| 0, _ => u_str
|
||||
|
@ -295,7 +294,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
|
|||
|
||||
A `_` symbol in the AST indicates automatic deductions not present in the original expression.
|
||||
-/
|
||||
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
|
||||
partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
|
||||
self expr
|
||||
where
|
||||
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
|
||||
|
@ -334,9 +333,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
|
|||
let name := mvarId.name
|
||||
pure s!"(:{pref} {name})"
|
||||
| .sort level =>
|
||||
let level := serializeSortLevel level sanitize
|
||||
let level := serializeSortLevel level
|
||||
pure s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
let declName := serializeName declName (sanitize := false)
|
||||
-- The universe level of the const expression is elided since it should be
|
||||
-- inferrable from surrounding expression
|
||||
pure s!"(:c {declName})"
|
||||
|
@ -369,7 +369,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
|
|||
-- is wrapped in a :lit sexp.
|
||||
let v' := match v with
|
||||
| .natVal val => toString val
|
||||
| .strVal val => s!"\"{val}\""
|
||||
| .strVal val => IR.EmitC.quoteString val
|
||||
pure s!"(:lit {v'})"
|
||||
| .mdata _ inner =>
|
||||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
|
@ -384,9 +384,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
|
|||
-- Elides all unhygenic names
|
||||
binderInfoSexp : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
| .implicit => " :implicit"
|
||||
| .strictImplicit => " :strictImplicit"
|
||||
| .instImplicit => " :instImplicit"
|
||||
| .implicit => " :i"
|
||||
| .strictImplicit => " :si"
|
||||
| .instImplicit => " :ii"
|
||||
|
||||
def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
|
||||
let pp?: Option String ← match options.printExprPretty with
|
||||
|
@ -532,7 +532,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
|
|||
then instantiateAll decl.type
|
||||
else pure $ decl.type
|
||||
let type_sexp ← if options.printSexp then
|
||||
let sexp ← serializeExpressionSexp type (sanitize := false)
|
||||
let sexp ← serializeExpressionSexp type
|
||||
pure <| " " ++ sexp
|
||||
else
|
||||
pure ""
|
||||
|
|
|
@ -58,7 +58,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
|
|||
| none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
|
||||
| some info => pure info
|
||||
let module? := env.getModuleIdxFor? name >>=
|
||||
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
|
||||
(λ idx => env.allImportedModuleNames.get? idx.toNat)
|
||||
let value? := match args.value?, info with
|
||||
| .some true, _ => info.value?
|
||||
| .some false, _ => .none
|
||||
|
@ -80,7 +80,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
|
|||
then value?.map (λ e =>
|
||||
e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
|
||||
else .none,
|
||||
module? := module?
|
||||
module? := module?.map (·.toString)
|
||||
}
|
||||
let result ← match info with
|
||||
| .inductInfo induct => pure { core with inductInfo? := .some {
|
||||
|
@ -113,6 +113,20 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
|
|||
k := r.k,
|
||||
} }
|
||||
| _ => pure core
|
||||
let result ← if args.source?.getD false then
|
||||
let srcSearchPath ← initSrcSearchPath
|
||||
let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
|
||||
let declRange? ← findDeclarationRanges? name
|
||||
let sourceStart? := declRange?.map (·.range.pos)
|
||||
let sourceEnd? := declRange?.map (·.range.endPos)
|
||||
.pure {
|
||||
result with
|
||||
sourceUri?,
|
||||
sourceStart?,
|
||||
sourceEnd?,
|
||||
}
|
||||
else
|
||||
.pure result
|
||||
return .ok result
|
||||
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
|
|
|
@ -104,14 +104,20 @@ structure InfoWithContext where
|
|||
info: Elab.Info
|
||||
context?: Option Elab.ContextInfo := .none
|
||||
|
||||
private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
|
||||
structure GoalCollectionOptions where
|
||||
collectTypeErrors : Bool := false
|
||||
|
||||
private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOptions := {})
|
||||
: IO (List InfoWithContext) := do
|
||||
let infos ← t.findAllInfoM none fun i ctx? => match i with
|
||||
| .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
|
||||
| .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
|
||||
let .some ctx := ctx? | return (false, true)
|
||||
if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
|
||||
if expectedType?.isNone then
|
||||
throw $ .userError "Sorry of indeterminant type is not allowed"
|
||||
return (true, false)
|
||||
unless options.collectTypeErrors do
|
||||
return (false, true)
|
||||
let .some expectedType := expectedType? | return (false, true)
|
||||
let typeMatch ← ctx.runMetaM lctx do
|
||||
let type ← Meta.inferType expr
|
||||
|
@ -130,8 +136,9 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
|
|||
|
||||
-- NOTE: Plural deliberately not spelled "sorries"
|
||||
@[export pantograph_frontend_collect_sorrys_m]
|
||||
def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
|
||||
return (← step.trees.mapM collectSorrysInTree).join
|
||||
def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
|
||||
: IO (List InfoWithContext) := do
|
||||
return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).join
|
||||
|
||||
structure AnnotatedGoalState where
|
||||
state : GoalState
|
||||
|
|
|
@ -183,7 +183,8 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
|
|||
-- to one of these seed mvars, it means an error has occurred when a tactic
|
||||
-- was executing on `src`. `evalTactic`, will not capture these mvars, so we
|
||||
-- need to manually find them and save them into the goal list.
|
||||
let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src)
|
||||
|
||||
let descendants ← Meta.getMVars (.mvar src)
|
||||
--let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
|
||||
let mut alreadyVisited : MVarIdSet := {}
|
||||
let mut result : MVarIdSet := {}
|
||||
|
|
|
@ -5,6 +5,7 @@ Note that no command other than `InteractionError` may have `error` as one of
|
|||
its field names to avoid confusion with error messages generated by the REPL.
|
||||
-/
|
||||
import Lean.Data.Json
|
||||
import Lean.Data.Position
|
||||
|
||||
namespace Pantograph.Protocol
|
||||
|
||||
|
@ -121,11 +122,13 @@ structure EnvCatalogResult where
|
|||
-- Print the type of a symbol
|
||||
structure EnvInspect where
|
||||
name: String
|
||||
-- If true/false, show/hide the value expressions; By default definitions
|
||||
-- values are shown and theorem values are hidden.
|
||||
-- Show the value expressions; By default definitions values are shown and
|
||||
-- theorem values are hidden.
|
||||
value?: Option Bool := .some false
|
||||
-- If true, show the type and value dependencies
|
||||
-- Show the type and value dependencies
|
||||
dependency?: Option Bool := .some false
|
||||
-- Show source location
|
||||
source?: Option Bool := .some false
|
||||
deriving Lean.FromJson
|
||||
-- See `InductiveVal`
|
||||
structure InductInfo where
|
||||
|
@ -172,6 +175,11 @@ structure EnvInspectResult where
|
|||
inductInfo?: Option InductInfo := .none
|
||||
constructorInfo?: Option ConstructorInfo := .none
|
||||
recursorInfo?: Option RecursorInfo := .none
|
||||
|
||||
-- Location in source
|
||||
sourceUri?: Option String := .none
|
||||
sourceStart?: Option Lean.Position := .none
|
||||
sourceEnd?: Option Lean.Position := .none
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure EnvAdd where
|
||||
|
@ -319,11 +327,13 @@ structure FrontendProcess where
|
|||
-- One of these two must be supplied: Either supply the file name or the content.
|
||||
fileName?: Option String := .none
|
||||
file?: Option String := .none
|
||||
-- If set to true, collect tactic invocations
|
||||
-- collect tactic invocations
|
||||
invocations: Bool := false
|
||||
-- If set to true, collect `sorry`s
|
||||
-- collect `sorry`s
|
||||
sorrys: Bool := false
|
||||
-- If set to true, extract new constants
|
||||
-- collect type errors
|
||||
typeErrorsAsGoals: Bool := false
|
||||
-- list new constants from each compilation step
|
||||
newConstants: Bool := false
|
||||
deriving Lean.FromJson
|
||||
structure InvokedTactic where
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
namespace Pantograph
|
||||
|
||||
@[export pantograph_version]
|
||||
def version := "0.2.23"
|
||||
def version := "0.2.24"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -265,7 +265,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
else
|
||||
pure .none
|
||||
let sorrys ← if args.sorrys then
|
||||
Frontend.collectSorrys step
|
||||
Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
|
||||
else
|
||||
pure []
|
||||
let messages ← step.messageStrings
|
||||
|
|
|
@ -143,6 +143,8 @@ def runTest (t: TestT m Unit): m LSpec.TestSeq :=
|
|||
Prod.snd <$> t.run LSpec.TestSeq.done
|
||||
def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
|
||||
t.run LSpec.TestSeq.done
|
||||
def runTestCoreM (env: Environment) (coreM: TestT CoreM Unit) (options: Array String := #[]): IO LSpec.TestSeq := do
|
||||
runCoreMSeq env (runTest coreM) options
|
||||
|
||||
end Monadic
|
||||
|
||||
|
|
|
@ -35,7 +35,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
|
|||
("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
|
||||
-- These ones are normal and easy
|
||||
("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
|
||||
("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
|
||||
("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :i) :i)"),
|
||||
-- Handling of higher order types
|
||||
("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
|
||||
("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
|
||||
|
@ -50,8 +50,8 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
|
|||
let entries: List (String × (List Name) × String) := [
|
||||
("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
|
||||
("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
|
||||
("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
|
||||
("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
|
||||
("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
|
||||
("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
|
||||
("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
|
||||
]
|
||||
entries.foldlM (λ suites (source, levels, target) =>
|
||||
|
@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
|
|||
.default)
|
||||
.implicit)
|
||||
.implicit,
|
||||
"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
|
||||
"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
|
||||
),
|
||||
]
|
||||
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
|
||||
|
|
|
@ -97,11 +97,26 @@ def test_inspect: IO LSpec.TestSeq := do
|
|||
) LSpec.TestSeq.done
|
||||
runCoreMSeq env inner
|
||||
|
||||
def test_symbol_location : TestT IO Unit := do
|
||||
let env: Environment ← importModules
|
||||
(imports := #[`Init])
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
addTest $ ← runTestCoreM env do
|
||||
let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
|
||||
checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
|
||||
|
||||
-- Doesn't work for symbols in `Init` for some reason
|
||||
--checkEq "file" result.sourceUri? <| .some "??"
|
||||
checkEq "pos" result.sourceStart? <| .some { line := 344, column := 0 }
|
||||
checkEq "pos" result.sourceEnd? <| .some { line := 344, column := 88 }
|
||||
|
||||
def suite: List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("Catalog", test_catalog),
|
||||
("Symbol Visibility", test_symbol_visibility),
|
||||
("Inspect", test_inspect),
|
||||
("Symbol Location", runTest test_symbol_location),
|
||||
]
|
||||
|
||||
end Pantograph.Test.Environment
|
||||
|
|
|
@ -6,11 +6,12 @@ import Test.Common
|
|||
open Lean Pantograph
|
||||
namespace Pantograph.Test.Frontend
|
||||
|
||||
def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
|
||||
def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
|
||||
: MetaM (List GoalState) := do
|
||||
let filename := "<anonymous>"
|
||||
let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
|
||||
let m := Frontend.mapCompilationSteps λ step => do
|
||||
return (step.before, ← Frontend.collectSorrys step)
|
||||
return (step.before, ← Frontend.collectSorrys step options)
|
||||
let li ← m.run context |>.run' state
|
||||
let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
|
||||
if sorrys.isEmpty then
|
||||
|
@ -181,9 +182,10 @@ def test_capture_type_mismatch : TestT MetaM Unit := do
|
|||
let input := "
|
||||
def mystery (k: Nat) : Nat := true
|
||||
"
|
||||
let goalStates ← (collectSorrysFromSource input).run' {}
|
||||
let options := { collectTypeErrors := true }
|
||||
let goalStates ← (collectSorrysFromSource input options).run' {}
|
||||
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
|
||||
checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
|
||||
checkEq "goals" ((← goalState.serializeGoals).map (·.devolatilize)) #[
|
||||
{
|
||||
target := { pp? := "Nat" },
|
||||
vars := #[{
|
||||
|
@ -193,6 +195,16 @@ def mystery (k: Nat) : Nat := true
|
|||
}
|
||||
]
|
||||
|
||||
def test_capture_type_mismatch_in_binder : TestT MetaM Unit := do
|
||||
let input := "
|
||||
example (p: Prop) (h: (∀ (x: Prop), Nat) → p): p := h (λ (y: Nat) => 5)
|
||||
"
|
||||
let options := { collectTypeErrors := true }
|
||||
let goalStates ← (collectSorrysFromSource input options).run' {}
|
||||
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
|
||||
checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
|
||||
]
|
||||
|
||||
def collectNewConstants (source: String) : MetaM (List (List Name)) := do
|
||||
let filename := "<anonymous>"
|
||||
let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
|
||||
|
@ -227,6 +239,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
|
|||
("sorry_in_coupled", test_sorry_in_coupled),
|
||||
("environment_capture", test_environment_capture),
|
||||
("capture_type_mismatch", test_capture_type_mismatch),
|
||||
--("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),
|
||||
("collect_one_constant", test_collect_one_constant),
|
||||
("collect_one_theorem", test_collect_one_theorem),
|
||||
]
|
||||
|
|
|
@ -174,6 +174,7 @@ def test_frontend_process : Test :=
|
|||
("file", .str file),
|
||||
("invocations", .bool true),
|
||||
("sorrys", .bool false),
|
||||
("typeErrorsAsGoals", .bool false),
|
||||
("newConstants", .bool false),
|
||||
]
|
||||
({
|
||||
|
@ -215,6 +216,7 @@ def test_frontend_process_sorry : Test :=
|
|||
("file", .str file),
|
||||
("invocations", .bool false),
|
||||
("sorrys", .bool true),
|
||||
("typeErrorsAsGoals", .bool false),
|
||||
("newConstants", .bool false),
|
||||
]
|
||||
({
|
||||
|
|
|
@ -97,7 +97,7 @@ def test_identity: TestM Unit := do
|
|||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
|
||||
#[inner])
|
||||
let state1parent ← state1.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
|
||||
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
|
||||
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
|
||||
|
||||
-- Individual test cases
|
||||
|
@ -259,7 +259,7 @@ def test_or_comm: TestM Unit := do
|
|||
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
|
||||
|
||||
let state1parent ← state1.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
|
||||
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
|
||||
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
|
||||
let tactic := "cases h"
|
||||
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
|
||||
|
@ -276,7 +276,7 @@ def test_or_comm: TestM Unit := do
|
|||
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
|
||||
|
||||
let state2parent ← state2.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
|
||||
serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
|
||||
let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
|
||||
let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
|
||||
let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
|
||||
|
@ -292,7 +292,7 @@ def test_or_comm: TestM Unit := do
|
|||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let state3_1parent ← state3_1.withParentContext do
|
||||
serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
|
||||
serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
|
||||
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
|
||||
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
|
||||
let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
|
||||
|
|
Loading…
Reference in New Issue