Idrisが2つの値が等しくないことを自動的に証明する方法を教えてください。 p : Not (Int = String)
p = \Refl impossible
この証明を自動的に生成するにはどうすればよいですか? autoは、Notを含むステートメントを証明することはできないようです。私の最終目標は、Idrisがベクトルのすべての要素が一意であり、2つのベクトルが互いに素であることを自
inf : Nat
inf = S inf
minimum' : Lazy Nat -> Lazy Nat -> Lazy Nat
minimum' Z b = Z
minimum' b Z = Z
minimum' (S a) (S b) = S (minimum' a b)
main : IO()
main = do
print $ Force $ minimum'
2つの自然な引数をとり、それらの等価性の証明の多分を返す関数を書いてみたいと思います。 私は equal : (a: Nat) -> (b: Nat) -> Maybe ((a == b) = True)
equal a b = case (a == b) of
True => Just Refl
False => Nothing
にしようとしているが、私はこれを行うには
これは失敗します。 > the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair
(input):1:5:When checking argument value to function Prelude.Basics.the:
Type mismatch between
A -> B1 -> (A, B1) (