Commit 3c204e66 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

add Decl.find_prop (along with find_constructors and find_inductive_cases)

parent ee4e0a01
......@@ -494,7 +494,7 @@ let check_decl kn d = match d.d_node with
let find_constructors kn ts =
match (Mid.find ts.ts_name kn).d_node with
| Dtype dl ->
begin match List.assoc ts dl with
begin match List.assq ts dl with
| Talgebraic cl -> cl
| Tabstract -> []
end
......@@ -502,10 +502,18 @@ let find_constructors kn ts =
let find_inductive_cases kn ps =
match (Mid.find ps.ls_name kn).d_node with
| Dind dl -> List.assoc ps dl
| Dind dl -> List.assq ps dl
| Dlogic _ -> []
| _ -> assert false
let find_prop kn pr =
match (Mid.find pr.pr_name kn).d_node with
| Dind dl ->
let test (_,l) = List.mem_assq pr l in
List.assq pr (snd (List.find test dl))
| Dprop (_,pr,f) -> f
| _ -> assert false
exception NonExhaustiveExpr of (pattern list * expr)
let rec check_matchT kn () t = match t.t_node with
......
......@@ -135,4 +135,5 @@ exception NonExhaustiveExpr of (pattern list * expr)
val find_constructors : known_map -> tysymbol -> lsymbol list
val find_inductive_cases : known_map -> lsymbol -> prop list
val find_prop : known_map -> prsymbol -> fmla
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment