Skip to content
Snippets Groups Projects
Commit df66bc4c authored by Boris Yakobowski's avatar Boris Yakobowski
Browse files

Adapt to branch feature/boris/valid-function-predicate

parent c25373c0
No related branches found
No related tags found
No related merge requests found
......@@ -310,6 +310,7 @@ module rec Transfer
| Pfresh _ -> Error.not_yet "\\fresh"
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
| Pvalid_function _ -> Error.not_yet "\\valid_function"
| Ptrue | Pfalse | Papp _ | Prel _
| Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
| Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
......
......@@ -564,6 +564,7 @@ and named_predicate_content_to_exp ?name kf env p =
| Papp _ -> not_yet env "logic function application"
| Pseparated _ -> not_yet env "\\separated"
| Pdangling _ -> not_yet env "\\dangling"
| Pvalid_function _ -> not_yet env "\\valid_function"
| Prel(rel, t1, t2) ->
let e, env =
comparison_to_exp ~loc kf env (relation_to_binop rel) t1 t2 None
......
......@@ -452,6 +452,7 @@ let rec type_predicate_named p =
| Papp _ -> Error.not_yet "logic function application"
| Pseparated _ -> Error.not_yet "\\separated"
| Pdangling _ -> Error.not_yet "\\dangling"
| Pvalid_function _ -> Error.not_yet "\\valid_function"
| Prel(_, t1, t2) ->
ignore (type_term t1);
ignore (type_term t2)
......
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