Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions KLR/Trace/Builtin.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ open Lean Elab Command Term Meta

def nki_ : Name := .str .anonymous "nki"
def nki_isa : Name := .str nki_ "isa"
def nki_stdlib : Name := .str nki_ "stdlib"
def nki_lang : Name := .str nki_ "language"
def nki_typing : Name := .str nki_ "typing"

Expand Down
1 change: 1 addition & 0 deletions KLR/Trace/NKI.lean
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ def NKIEnv : List (Name × Term) :=
[ module nki_
, module nki_isa
, module nki_lang
, module nki_stdlib
, module nki_typing
, module `math
, module `numpy
Expand Down
1 change: 0 additions & 1 deletion KLR/Trace/Term.lean
Original file line number Diff line number Diff line change
Expand Up @@ -678,6 +678,5 @@ def builtinEnv : List (Name × Term) := Id.run do
| .str `builtin.python n => [.str `builtins n, .str .anonymous n]
| .str `builtin.isa n => [nisa n, name]
| .str `builtin.typing n => [nt n, name]
| .str `builtin.lang n => [nl n, name]
| _ => [name]
names.map fun n => (n, fn)
Loading