search

markokoleznik / agda-writer

A simple GUI for Agda
Other
31 stars 2 forks source link

Load deletes {| ... |} #11

Closed andrejbauer closed 9 years ago

andrejbauer commented 9 years ago

On Load in the following code sup ? disappears:

 module Foo where

 data bool : Set where
   false : bool
   true : bool

 or : bool -> bool -> bool
 or false y = y
 or true _ = true

 data N : Set where
   zero : N
   succ : N -> N

 data Ordinal : Set where
   zer : Ordinal
   suc : Ordinal -> Ordinal
   sup : (N -> Ordinal) -> Ordinal

 sum : Ordinal -> Ordinal -> Ordinal
 sum zer y = y
 sum (suc x) y = suc (sum x y)
 sum (sup xs) y = {! sup ? !}
andrejbauer commented 9 years ago

Probably related to #12

markokoleznik commented 9 years ago

Fixed with #8. I have no idea why I deleted those goals by hand, I should know that Agda know better when goals are returned :)