Package fj.data.hlist
Class HPre.HEq<X,Y,B extends HPre.HBool>
java.lang.Object
fj.data.hlist.HPre.HEq<X,Y,B>
- Enclosing class:
HPre
Type-level equality. Represents evidence for X and Y being equal, or counterevidence against.
-
Field Summary
Fields -
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionstatic <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) A number is equal to another if their predecessors are equal.static <N extends HPre.HNat<N>>
HPre.HEq<HPre.HSucc<N>, HPre.HZero, HPre.HFalse> eq
(HPre.HSucc<N> a, HPre.HZero b) Zero is not equal to anything other than zero.static <N extends HPre.HNat<N>>
HPre.HEq<HPre.HZero, HPre.HSucc<N>, HPre.HFalse> 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.v()
-
Field Details
-
v
-
-
Constructor Details
-
HEq
-
-
Method Details
-
v
-
eq
Zero is equal to itself.- Parameters:
a
- Zerob
- Zero- Returns:
- Equality for Zero
-
eq
public static <N extends HPre.HNat<N>> HPre.HEq<HPre.HZero,HPre.HSucc<N>, eqHPre.HFalse> (HPre.HZero a, HPre.HSucc<N> b) Zero is not equal to anything other than zero. -
eq
public static <N extends HPre.HNat<N>> HPre.HEq<HPre.HSucc<N>,HPre.HZero, eqHPre.HFalse> (HPre.HSucc<N> a, HPre.HZero b) Zero is not equal to anything other than zero. -
eq
public static <N extends HPre.HNat<N>,NN extends HPre.HNat<NN>, HPre.HEq<HPre.HSucc<N>,B extends HPre.HBool, E extends HPre.HEq<N, NN, B>> HPre.HSucc<NN>, eqB> (HPre.HSucc<N> a, HPre.HSucc<NN> b, E e) A number is equal to another if their predecessors are equal.
-