public static final class HPre.HEq<X,Y,B extends HPre.HBool>
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
static <N extends HPre.HNat<N>,NN extends HPre.HNat<NN>,B extends HPre.HBool,E extends HPre.HEq<N,NN,B>> |
eq(HPre.HSucc<N> a,
HPre.HSucc<NN> b,
E e)
A number is equal to another if their predecessors are equal.
|
static <N extends HPre.HNat<N>> |
eq(HPre.HSucc<N> a,
HPre.HZero b)
Zero is not equal to anything other than zero.
|
static <N extends HPre.HNat<N>> |
eq(HPre.HZero a,
HPre.HSucc<N> b)
Zero is not equal to anything other than zero.
|
static HPre.HEq<HPre.HZero,HPre.HZero,HPre.HTrue> |
eq(HPre.HZero a,
HPre.HZero b)
Zero is equal to itself.
|
B |
v() |
public B v()
public static HPre.HEq<HPre.HZero,HPre.HZero,HPre.HTrue> eq(HPre.HZero a, HPre.HZero b)
a
- Zerob
- Zeropublic static <N extends HPre.HNat<N>> HPre.HEq<HPre.HZero,HPre.HSucc<N>,HPre.HFalse> eq(HPre.HZero a, HPre.HSucc<N> b)
public static <N extends HPre.HNat<N>> HPre.HEq<HPre.HSucc<N>,HPre.HZero,HPre.HFalse> eq(HPre.HSucc<N> a, HPre.HZero b)
public static <N extends HPre.HNat<N>,NN extends HPre.HNat<NN>,B extends HPre.HBool,E extends HPre.HEq<N,NN,B>> HPre.HEq<HPre.HSucc<N>,HPre.HSucc<NN>,B> eq(HPre.HSucc<N> a, HPre.HSucc<NN> b, E e)