exception LRefNotFound of Brg.message
-type ho_whd_result =
- | Sort of int
- | Abst of Brg.term
-
-val ho_whd:
- (Brg.context -> ho_whd_result -> 'a) -> Brg.context -> Brg.term -> 'a
+val domain:
+ (Brg.term option -> 'a) -> Brg.context -> Brg.term -> 'a
val are_convertible:
- (bool -> 'a) -> Brg.context -> Brg.term -> Brg.term -> 'a
+ (bool -> 'a) -> ?si:bool -> Brg.context -> Brg.term -> Brg.term -> 'a