kdrag
- Calc
- FreshVar()
- FreshVars()
- Inductive()
- Lemma()
- NewType()
- PTheorem()
- Proof
- QExists()
- QForAll()
- QImplies()
- Struct()
- Theorem()
- axiom()
- cond()
- define()
- prove()
- search()
- simp()
- kdrag.all
- kdrag.config
- kdrag.contrib
- kdrag.datatype
- kdrag.hypothesis
- kdrag.kernel
- kdrag.modal
- kdrag.notation
  - kdrag.notation.ExistsUnique
    - ExistsUnique()
  - kdrag.notation.GenericDispatch
  - kdrag.notation.QExists
  - kdrag.notation.QForAll
  - kdrag.notation.QImplies
  - kdrag.notation.QLambda
  - kdrag.notation.cond
  - kdrag.notation.conde
  - kdrag.notation.quantifier_call
  - Cond
  - ExistsUnique()
  - GenericDispatch()
  - QExists()
  - QForAll()
  - QImplies()
  - QLambda()
  - SortDispatch
  - add
  - and_
  - call
  - choose
  - cond()
  - conde()
  - div
  - eq
  - exists
  - forall
  - ge
  - getitem
  - gt
  - induct
  - invert
  - le
  - lt
  - matmul
  - measure
  - mul
  - ne
  - neg
  - or_
  - quantifier_call()
  - radd
  - rmul
  - sub
  - to_int
  - to_real
  - wf
- kdrag.parsers
- kdrag.printers
- kdrag.property
- kdrag.reflect
- kdrag.rewrite
- kdrag.smt
- kdrag.solvers
- kdrag.tactics
- kdrag.tele
- kdrag.theories
- kdrag.utils

knuckledragger

kdrag
kdrag.notation
kdrag.notation.ExistsUnique
View page source

kdrag.notation.ExistsUnique

kdrag.notation.ExistsUnique(v: ExprRef, *concs) → BoolRef

Unique Existence

Parameters:: v (ExprRef)
Return type:: BoolRef

Previous Next

© Copyright 2024, Philip Zucker.

Built with Sphinx using a theme provided by Read the Docs.