Suppose I have two props, P1 and P2. Is there an easy way of reflecting into bool in such a way that if P1 and P2 are definitionally equal, I get true, and if P1 and P2 are not definitionally equal, I get false? It feels like there should be because definitional equality should be decidable, but I don't know of a way of doing it.

if they are definitionally equal, you pick true

otherwise you pick false

this is at the meta level of course

I mean is there a way of writing a function that computes this

no

suppose `f : Prop -> Prop -> bool`

was that function

under context `x, y : Prop`

, `f x y`

computes to false, but when `x`

and `y`

are substituted with `True`

the value changes to `true`

such a behaviour would be broken

Indeed what you want seems too general Chris, what are you trying to prove?

I have non empty list(k::t) and two hypothesis. H1: k <= list_max (k::t) & H2: list_max (k::t) <=k.

From these H1 and H2 , is it possible list_max (k::t) =k?

Last updated: Jun 22 2024 at 16:02 UTC