Class HPre.HEq<X, Y, B extends HPre.HBool>

java.lang.Object

fj.data.hlist.HPre.HEq<X,Y,B>

Enclosing class:

HPre

public static final class HPre.HEq<X, Y, B extends HPre.HBool>
extends Object

Type-level equality. Represents evidence for X and Y being equal, or counterevidence against.

Field Summary

Fields

Modifier and Type	Field	Description
private final B	v

Constructor Summary

Constructors

Modifier	Constructor	Description
private	HEq(B v)

Method Summary

Modifier and Type	Method	Description
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)	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.
B	v()

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

v

private final B extends HPre.HBool v

Constructor Details

HEq

private HEq(B v)

Method Details

v

public B v()

eq

public static HPre.HEq<HPre.HZero, HPre.HZero, HPre.HTrue> eq(HPre.HZero a,
 HPre.HZero b)

Zero is equal to itself.

Parameters:

a - Zero

b - Zero

Returns:

Equality for Zero

eq

public 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.

eq

public 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.

eq

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)

A number is equal to another if their predecessors are equal.