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

feat: Add definitions and theorems to the environment #41

Merged
aniva merged 9 commits from env/add-decl into dev 2023-12-26 12:41:02 -08:00
Conversation 0 Commits 9 Files Changed 10 +2 -2
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 2f3a91562a - Show all commits

4
Pantograph.lean
View File

@ -105,14 +105,14 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let type ← match syntax_from_str env args.type with let type ← match syntax_from_str env args.type with
| .ok syn => do | .ok syn => do
match ← syntax_to_expr syn with match ← (syntax_to_expr syn |> runTermElabM) with
| .error e => return .error $ errorExpr e | .error e => return .error $ errorExpr e
| .ok expr => pure expr | .ok expr => pure expr
| .error e => return .error $ errorExpr e | .error e => return .error $ errorExpr e
let value ← match syntax_from_str env args.value with let value ← match syntax_from_str env args.value with
| .ok syn => do | .ok syn => do
try try
let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) |> runTermElabM
pure $ expr pure $ expr
catch ex => return .error $ errorExpr (← ex.toMessageData.toString) catch ex => return .error $ errorExpr (← ex.toMessageData.toString)
| .error e => return .error $ errorExpr e | .error e => return .error $ errorExpr e