1361d733a6
This PR makes the external checker lean4checker available as the existing `leanchecker` binary already known to elan, allowing for out-of-the-box access to it. --------- Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
22 lines
561 B
Text
22 lines
561 B
Text
import LeanCheckerTests.OpenPrivate
|
|
|
|
set_option Elab.async false
|
|
|
|
open private Lean.Kernel.Environment.add from Lean.Environment
|
|
open private Lean.Environment.setCheckedSync from Lean.Environment
|
|
|
|
open Lean in
|
|
run_elab
|
|
let env ← getEnv
|
|
let kenv := env.toKernelEnv
|
|
let kenv := Lean.Kernel.Environment.add kenv <| .ctorInfo {
|
|
name := `False.intro
|
|
levelParams := []
|
|
type := .const ``False []
|
|
induct := `False
|
|
cidx := 0
|
|
numParams := 0
|
|
numFields := 0
|
|
isUnsafe := false
|
|
}
|
|
setEnv <| Lean.Environment.setCheckedSync env kenv
|