Agda2> (agda2-status-action "")
Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Long (Long.agda).\n" t)
(agda2-info-action "*Type-checking*" "Finished Long.\n" t)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Maybe Nat\n?1 : Maybe Nat\n?2 : Nat\n?3 : D ?2\n?4 : D z\n?5 : Set\n?6 : Maybe ?5\n" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> (agda2-status-action "")
(agda2-highlight-load-and-delete-action "
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Long (Long.agda).\n" t)
(agda2-info-action "*Type-checking*" "Finished Long.\n" t)
(agda2-status-action "")
(agda2-info-action "*Error*" "You can only compile modules without unsolved metavariables\nor termination checking problems.\n" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> Agda2> (agda2-status-action "")
(agda2-info-action "*Constraints*" "" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Long (Long.agda).\n" t)
(agda2-info-action "*Type-checking*" "Finished Long.\n" t)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Maybe Nat\n?1 : Maybe Nat\n?2 : Nat\n?3 : D ?2\n?4 : D z\n?5 : Set\n?6 : Maybe ?5\n" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Constraints*" "" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Maybe Nat\n?1 : Maybe Nat\n?2 : Nat\n?3 : D ?2\n?4 : D z\n?5 : Set\n?6 : Maybe ?5\n" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> Agda2> ((last . 2) . (agda2-make-case-action '("eval (val z) = ?" "eval (val (s n)) = ?")))
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> (agda2-give-action 0 "Just ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat\n?2 : Nat\n?3 : D ?2\n?4 : D z\n?5 : Set\n?6 : Maybe ?5\n?7 : Nat\n" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 4 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Intro*" "Don't know which constructor to introduce of z or s" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 4 5 6)))
Agda2> (agda2-give-action 4 "d")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat\n?2 : Nat\n?3 : D ?2\n?5 : Set\n?6 : Maybe ?5\n?7 : Nat\n" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Inferred Type*" "Nat → Set" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Context*" "n : Nat" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Current Goal*" "Nat" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: Nat\n————————————————————————————————————————————————————————————\nn : Nat" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: Nat\nHave: Nat\n————————————————————————————————————————————————————————————\nn : Nat" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Module contents*" "Modules\nNames\n  d : D z" nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
Agda2> (agda2-give-action 3 "d")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat\n?2 : Nat\n?5 : Set\n?6 : Maybe ?5\n?7 : Nat\n" nil)
((last . 1) . (agda2-goals-action '(7 1 2 5 6)))
Agda2> (agda2-give-action 6 "Just ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat\n?2 : Nat\n?5 : Set\n?7 : Nat\n?8 : ?5\n" nil)
((last . 1) . (agda2-goals-action '(7 1 2 5 8)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Normal Form*" "s′ z" nil)
((last . 1) . (agda2-goals-action '(7 1 2 5 8)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Normal Form*" "s z" nil)
((last . 1) . (agda2-goals-action '(7 1 2 5 8)))
Agda2> (agda2-give-action 8 "d")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat\n?2 : Nat\n?5 : Set\n?7 : Nat\n" nil)
((last . 1) . (agda2-goals-action '(7 1 2 5)))
Agda2> Agda2> ((last . 2) . (agda2-solveAll-action '(2 "z" 5 "D z")))
((last . 1) . (agda2-goals-action '(7 1 2 5)))
Agda2> (agda2-info-action "*Error*" "1,1-4\nNat !=< Maybe Nat of type Set\nwhen checking that the expression s z has type Maybe Nat" nil)
(agda2-status-action "")
Agda2> (agda2-status-action "")
(agda2-info-action "*Normal Form*" "?1" nil)
((last . 1) . (agda2-goals-action '(7 1 2 5)))
Agda2> (agda2-give-action 1 "Nothing")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : Nat\n?5 : Set\n?7 : Nat\n" nil)
((last . 1) . (agda2-goals-action '(7 2 5)))
Agda2> (agda2-give-action 7 "n")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : Nat\n?5 : Set\n" nil)
((last . 1) . (agda2-goals-action '(2 5)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Inferred Type*" "Maybe Nat" nil)
((last . 1) . (agda2-goals-action '(2 5)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Normal Form*" "Nothing" nil)
((last . 1) . (agda2-goals-action '(2 5)))
Agda2> (agda2-info-action "*Error*" "1,4-5\nNot in scope:\n  n at 1,4-5\nwhen scope checking n" nil)
(agda2-status-action "")
Agda2> (agda2-status-action "")
(agda2-info-action "*Normal Form*" "s z" nil)
((last . 1) . (agda2-goals-action '(2 5)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Module contents*" "Modules\nNames\n  d : D z" nil)
((last . 1) . (agda2-goals-action '(2 5)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Long (Long.agda).\n" t)
(agda2-info-action "*Type-checking*" "Finished Long.\n" t)
(agda2-status-action "")
(agda2-info-action "*Error*" "You can only compile modules without unsolved metavariables\nor termination checking problems.\n" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2> (agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-info-action "*Type-checking*" "Checking Long (Long.agda).\n" t)
(agda2-info-action "*Type-checking*" "Finished Long.\n" t)
(agda2-status-action "")
(agda2-info-action "*Error*" "You can only compile modules without unsolved metavariables\nor termination checking problems.\n" nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
Agda2>