module Rmin where
infix 4 _≡_
infixl 4 _>_ _<_
infixr 1 _∨_
postulate ℝ : Set
------------------------------------------------------------------------------
-- Logic stuff
-- The identity type on the universe of discourse.
data _≡_ (x : ℝ) : ℝ → Set where
refl : x ≡ x
data _∨_ (A B : Set) : Set where
inj₁ : A → A ∨ B
inj₂ : B → A ∨ B
case : ∀ {A B} → {C : Set} → (A → C) → (B → C) → A ∨ B → C
case f g (inj₁ a) = f a
case f g (inj₂ b) = g b
------------------------------------------------------------------------------
-- Real numbers stuff
postulate _>_ : ℝ → ℝ → Set
_<_ : ℝ → ℝ → Set
y < x = x > y
{-# ATP definition _<_ #-}
postulate
trichotomy : (x y : ℝ) → (x > y) ∨ (x ≡ y) ∨ (x < y)
{-# ATP axiom trichotomy #-}
------------------------------------------------------------------------------
rmin : ℝ → ℝ → ℝ
rmin x y = case (λ _ → y) (λ h → case (λ _ → x) (λ _ → x) h) (trichotomy x y)
{-# ATP definition rmin #-}
postulate foo : ∀ x y → rmin x y ≡ rmin x y
{-# ATP prove foo #-}
$ agda Rmin
$ apia --check Rmin.agda
apia: tptp4X found an error/warning in the file /tmp/Rmin/43-foo.fof
Please report this as a bug
WARNING: Line 34 Char 155 Token "," : Multiple arity symbol n_62__46_251303045, arity 0 and now 2
WARNING: Line 34 Char 225 Token ")" : Multiple arity symbol n_60__48_251303045, arity 0 and now 2
WARNING: Line 34 Char 313 Token "," : Multiple arity symbol n_60__48_251303045, arity 0 and now 2
WARNING: Line 34 Char 366 Token ")" : Multiple arity symbol case_32_251303045, arity 5 and now 6
WARNING: Line 45 Char 77 Token "=" : Multiple arity symbol rmin_60_251303045, arity 5 and now 2
WARNING: Line 45 Char 100 Token ")" : Multiple arity symbol rmin_60_251303045, arity 5 and now 2
From @asr on November 24, 2015 10:34