package why3

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

exception ConstructorExpected of Term.lsymbol * Ty.ty

exception NonExhaustive of Term.pattern list

val compile : 
  get_constructors:(Ty.tysymbol -> Term.lsymbol list) ->
  mk_case:(Term.term -> (Term.pattern * 'a) list -> 'a) ->
  mk_let:(Term.vsymbol -> Term.term -> 'a -> 'a) ->
  Term.term list ->
  (Term.pattern list * 'a) list ->
  'a

val compile_bare : 
  mk_case:(Term.term -> (Term.pattern * 'a) list -> 'a) ->
  mk_let:(Term.vsymbol -> Term.term -> 'a -> 'a) ->
  Term.term list ->
  (Term.pattern list * 'a) list ->
  'a

val check_compile : 
  get_constructors:(Ty.tysymbol -> Term.lsymbol list) ->
  Term.term list ->
  Term.pattern list list ->
  unit

val is_exhaustive : Term.term list -> Term.pattern list list -> bool