Revision 9d08a76fb50773e0b6b1afad31f37dfb821fee75 authored by Benjamin Gregoire on 24 November 2022, 16:10:02 UTC, committed by Benjamin Gregoire on 24 November 2022, 16:10:02 UTC
1 parent 69c9c2e
Raw File
ecHiPredicates.mli
(* -------------------------------------------------------------------- *)
open EcLocation
open EcSymbols
open EcParsetree

(* -------------------------------------------------------------------- *)
type tperror =
| TPE_Typing of EcTyping.tyerror
| TPE_TyNotClosed
| TPE_DuplicatedConstr of symbol

exception TransPredError of EcLocation.t * EcEnv.env * tperror

val tperror : EcLocation.t -> EcEnv.env -> tperror -> 'a

(* -------------------------------------------------------------------- *)
val trans_preddecl : EcEnv.env -> ppredicate located -> EcDecl.operator
back to top