Skip to content

Commit 8da0c15

Browse files
committed
Export base_{term,type}_assums from reflectionLib
although without the (I think useless?) vti parameter
1 parent 14987c2 commit 8da0c15

File tree

2 files changed

+5
-0
lines changed

2 files changed

+5
-0
lines changed

reflectionLib.sig

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ signature reflectionLib = sig include Abbrev
3030
val to_inner_prop : (hol_type,hol_type)Lib.subst -> hol_type -> term
3131
val base_types_of_term : term -> hol_type list
3232
val base_terms_of_term : term -> term list
33+
val base_type_assums : hol_type -> term list
34+
val base_term_assums : term -> term list
3335

3436
val prove_wf_to_inner : hol_type -> thm
3537

reflectionLib.sml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2628,4 +2628,7 @@ in
26282628
}
26292629
end
26302630
end
2631+
2632+
val base_term_assums = base_term_assums []
2633+
val base_type_assums = base_type_assums []
26312634
end

0 commit comments

Comments
 (0)