Skip to content
Snippets Groups Projects
Commit 51daaa18 authored by Michele Alberti's avatar Michele Alberti
Browse files

[interpretation] Rename interpretation theory.

parent df8cbb79
No related branches found
No related tags found
No related merge requests found
......@@ -52,7 +52,7 @@ let term_of_caisar_op engine op =
Term.t_app_infer (ls_of_caisar_op engine op) []
let caisar_env env cwd =
let th = Env.read_theory env [ "caisar" ] "Interpret" in
let th = Env.read_theory env [ "caisar" ] "Interpretation" in
let ts_dataset = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
{
dataset_ty = Ty.ty_app ts_dataset [];
......@@ -89,7 +89,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
in
[
( [ "caisar" ],
"Interpret",
"Interpretation",
[],
[ ("open_dataset", None, open_dataset); ("size", None, size) ] );
]
......
......@@ -81,7 +81,7 @@ theory NN
function relu (a: t): t = if a .> (0.0:t) then a else (0.0:t)
end
theory Interpret
theory Interpretation
use bool.Bool
use int.Int
......
Test interpret
$ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use caisar.Interpret
> use caisar.Interpretation
> use int.Int
>
> goal G1: 1+1=2
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment