ssreflect - Automatic proofs of is_true

Subject: Ssreflect Users Discussion List

List archive

Automatic proofs of is_true

From: Arthur Azevedo de Amorim <>
To:
Subject: Automatic proofs of is_true
Date: Tue, 16 Jun 2009 16:20:47 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=IacUvMc0mL2f1ovRdj0LI8l4XaLa9lTB5HvN0n0QWYkBvHCtFZToqBMz+yb52d+DF/ pyWeW/NhQykn7rMElISQ8QmAIYWaEN/6hMK2fpV78WejlE6y8KikYIQ4r7eFYFmZKr7O XonEnsXS3O8x5y+y46lBE8SxD1GLHjGuaMpgg=

Hello everyone,

is there a way in plain ssr to cast between I_n and I_m when (n <= m) is convertible to true without mentioning explicitly its proof, e.g, when using a value of I_3 in a context that asks for an I_5 without calling widen_ord and passing it (refl_equal _)?

Thanks in advance.

--
Arthur Azevedo de Amorim

Automatic proofs of is_true, Arthur Azevedo de Amorim, 06/16/2009
- RE: Automatic proofs of is_true, Georges Gonthier, 06/16/2009

List archive

Automatic proofs of is_true