aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
Conversation 6 Commits 41 Files Changed 22 +3 -3
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 3c90c94645 - Show all commits

6
Pantograph/Serial.lean
View File

@ -264,7 +264,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
name := ofName goal.name, name := ofName goal.name,
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
isConversion := isLHSGoal? mvarDecl.type |>.isSome, isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serializeExpression options (← instantiateMVars (← instantiate mvarDecl.type))), target := (← serializeExpression options (← instantiate mvarDecl.type)),
vars := vars.reverse.toArray vars := vars.reverse.toArray
} }
where where
@ -319,7 +319,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
else else
pure [] pure []
let type ← if options.instantiate let type ← if options.instantiate
then instantiateMVars decl.type then instantiateAll decl.type
else pure $ decl.type else pure $ decl.type
let type_sexp ← serializeExpressionSexp type (sanitize := false) let type_sexp ← serializeExpressionSexp type (sanitize := false)
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
@ -327,7 +327,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
if options.printValue then if options.printValue then
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
let value ← if options.instantiate let value ← if options.instantiate
then instantiateMVars value then instantiateAll value
else pure $ value else pure $ value
pure s!"\n := {← Meta.ppExpr value}" pure s!"\n := {← Meta.ppExpr value}"
else else