class ['a] status:
?history_size:int -> (** default 20 *)
?uri:UriManager.uri ->
- typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+ typ:Cic.term -> body:Cic.term Lazy.t -> metasenv:Cic.metasenv ->
attrs:Cic.attribute list ->
(proof_status -> 'a) -> (* init data *)
(proof_status * 'a -> proof_status -> 'a) -> (* update data *)
method proof: ProofEngineTypes.proof
method metasenv: Cic.metasenv
- method body: Cic.term
+ method body: Cic.term Lazy.t
method typ: Cic.term
method attrs: Cic.attribute list
val trivial_status:
?uri:UriManager.uri ->
- typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+ typ:Cic.term -> body:Cic.term Lazy.t -> metasenv:Cic.metasenv ->
attrs:Cic.attribute list ->
unit ->
unit status