(agda2-highlight-load-and-delete-action)
(agda2-status-action "")
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Maybe Nat ?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?4 : D′ z ?5 : Set ?6 : Maybe ?5 " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
(agda2-status-action "")
(agda2-highlight-load-and-delete-action)
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*Error*" "You need to fix the following errors before you can compile the module: Unsolved interaction metas at the following locations: Long.agda:21,16-17 Long.agda:22,16-17 Long.agda:29,9-13 Long.agda:30,7-11 Long.agda:33,7-11 Long.agda:35,13-17 Long.agda:36,7-11 " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
(agda2-status-action "")
(agda2-info-action "*Constraints*" "" nil)
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Maybe Nat ?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?4 : D′ z ?5 : Set ?6 : Maybe ?5 " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
(agda2-status-action "")
(agda2-info-action "*Constraints*" "" nil)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Maybe Nat ?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?4 : D′ z ?5 : Set ?6 : Maybe ?5 " nil)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : Maybe Nat ?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?4 : D z ?5 : Set ?6 : Maybe ?5 " nil)
((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-give-action 0 "Just ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?4 : D′ z ?5 : Set ?6 : Maybe ?5 ?7 : Nat " nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 4 5 6)))
(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-give-action 4 "d")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?5 : Set ?6 : Maybe ?5 ?7 : Nat " nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
(agda2-status-action "")
(agda2-info-action "*Inferred Type*" "Nat → Set" nil)
(agda2-status-action "")
(agda2-info-action "*Context*" "n : Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Current Goal*" "Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: Nat ———————————————————————————————————————————————————————————— n : Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: Nat ———————————————————————————————————————————————————————————— n : Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: Nat Have: Nat ———————————————————————————————————————————————————————————— n : Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Module contents*" "Modules Names d : D z" nil)
(agda2-status-action "")
(agda2-info-action "*Module contents*" "Modules D Exp Maybe Nat Names D : Nat → Set D′ : Nat → Set Exp : Set Just : {@0 A : Set} → A → Maybe A Maybe : Set → Set Nat : Set Nothing : {@0 A : Set} → Maybe A d : D z eval : Exp → Maybe Nat foo : D ?2 s : Nat → Nat s′ : Nat → Nat throw : Exp val : Nat → Exp z : Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Intro*" "No introduction forms found." nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 6)))
(agda2-give-action 6 "Just ?")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?5 : Set ?7 : Nat ?8 : ?5 " nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5 8)))
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "s′ z" nil)
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "s z" nil)
(agda2-give-action 8 "d")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : Maybe Nat ?2 : Nat ?3 : D ?2 ?5 : Set ?7 : Nat " nil)
((last . 1) . (agda2-goals-action '(7 1 2 3 5)))
((last . 2) . (agda2-solveAll-action '(5 "D z")))
((last . 1) . (agda2-goals-action '(7 1 2 3 5)))
(agda2-info-action "*Error*" "1,1-4 Nat !=< Maybe Nat when checking that the inferred type of an application Nat matches the expected type Maybe Nat" nil)
(agda2-highlight-load-and-delete-action)
(agda2-status-action "")
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "?1" nil)
(agda2-give-action 1 "Nothing")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : Nat ?3 : D ?2 ?5 : Set ?7 : Nat " nil)
((last . 1) . (agda2-goals-action '(7 2 3 5)))
(agda2-give-action 7 "n")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : Nat ?3 : D ?2 ?5 : Set " nil)
((last . 1) . (agda2-goals-action '(2 3 5)))
(agda2-status-action "")
(agda2-info-action "*Inferred Type*" "Maybe Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "Nothing" nil)
(agda2-info-action "*Error*" "1,4-5 Not in scope: n at 1,4-5 when scope checking n" nil)
(agda2-highlight-load-and-delete-action)
(agda2-status-action "")
(agda2-status-action "")
(agda2-info-action "*Normal Form*" "s z" nil)
(agda2-status-action "")
(agda2-info-action "*Module contents*" "Modules Names d : D z" nil)
(agda2-status-action "")
(agda2-info-action "*Module contents*" "Modules D Exp Maybe Nat Names D : Nat → Set D′ : Nat → Set Exp : Set Just : {@0 A : Set} → A → Maybe A Maybe : Set → Set Nat : Set Nothing : {@0 A : Set} → Maybe A bar : D′ z baz : Maybe (D z) d : D z eval : Exp → Maybe Nat foo : D ?2 s : Nat → Nat s′ : Nat → Nat throw : Exp val : Nat → Exp z : Nat" nil)
(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*Error*" "You need to fix the following errors before you can compile the module: Unsolved interaction metas at the following locations: Long.agda:21,16-17 Long.agda:22,16-17 Long.agda:29,9-13 Long.agda:30,7-11 Long.agda:33,7-11 Long.agda:35,13-17 Long.agda:36,7-11 " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6)))
