Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Relation.Binary.IsStrictTotalOrder Agda.Builtin.Equality._≡_ (StrictTotalOrder._<_ <-strictTotalOrder) " nil)
((last . 1) . (agda2-goals-action '(0)))
Agda2> (agda2-give-action 0 "(record { isEquivalence = record { refl = λ {x} → Agda.Builtin.Equality._≡_.refl ; sym = Relation.Binary.PropositionalEquality.Core.sym ; trans = Relation.Binary.PropositionalEquality.Core.trans } ; trans = Data.Nat.Properties.<-trans ; compare = Data.Nat.Properties.<-cmp })")
(agda2-status-action "")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
Agda2> 