Open
Description
For example, the following will stall when lpn is reached.
defn list : prop → prop
>| nil = list P
>| cons = P → list P → list P
defn lp : {P : prop} list P → prop
| lpn = lp nil
| lpc = {l : list P} {e : P} lp l → lp (cons e l)
By changing that line to | lpn = lp {P = P} nil, the stalling doesn't happen, but I think Caledon should be smart enough to know that P can't be inferred and report an error instead of stalling.
As an aside, this glitch doesn't occur for this program;
defn num : prop
>| zero = num
>| succ = [n : num] num
defn list : prop -> prop
>| nil = list P
>| cons = P -> list P -> list P
defn append : {P : prop} list P -> list P -> list P -> prop
| nila = {l : list P} append nil l l
| nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)
defn length : {P : prop} list P -> num -> prop
| lengthn = length nil zero
| lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)
nor this program
defn num : prop
>| zero = num
>| su
557A
cc = [n : num] num
defn list : prop -> prop
>| nil = list P
>| cons = P -> list P -> list P
defn last : {P : prop} list P -> P -> prop
| lastn = {e : P} last (cons e nil) e
| lastc = {l : list P} {le e : P} last l e -> last (cons le l) e
defn length : {P : prop} list P -> num -> prop
| lengthn = length nil zero
| lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)
but it does occur for this program
defn num : prop
>| zero = num
>| succ = [n : num] num
defn list : prop -> prop
>| nil = list P
>| cons = P -> list P -> list P
defn append : {P : prop} list P -> list P -> list P -> prop
| nila = {l : list P} append nil l l
| nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)
defn last : {P : prop} list P -> P -> prop
| lastn = {e : P} last (cons e nil) e
| lastc = {l : list P} {le e : P} last l e -> last (cons le l) e
defn length : {P : prop} list P -> num -> prop
| lengthn = length nil zero
| lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)
stalling on lengthn. This is an odd glitch which is clearly sensitive to context, but I'm not certain how to describe it beyond these examples.
Metadata
Metadata
Assignees
Labels
No labels