Compare commits
3 Commits
4aa3e5f730
...
00e79d4264
Author | SHA1 | Date |
---|---|---|
rhiannon morris | 00e79d4264 | |
rhiannon morris | a11bedd62a | |
rhiannon morris | c5fa11bdec |
|
@ -31,7 +31,7 @@ baseStr (UN x) = x
|
||||||
baseStr (MN x i) = "\{x}#\{show i}"
|
baseStr (MN x i) = "\{x}#\{show i}"
|
||||||
baseStr Unused = "_"
|
baseStr Unused = "_"
|
||||||
|
|
||||||
export Show BaseName where show = baseStr
|
export Show BaseName where show = show . baseStr
|
||||||
export FromString BaseName where fromString = UN
|
export FromString BaseName where fromString = UN
|
||||||
|
|
||||||
|
|
||||||
|
@ -82,7 +82,8 @@ fromPBaseName = MakeName [<] . UN
|
||||||
|
|
||||||
export
|
export
|
||||||
Show PName where
|
Show PName where
|
||||||
show (MakePName mods base) = concat $ intersperse "." $ toList $ mods :< base
|
show (MakePName mods base) =
|
||||||
|
show $ concat $ intersperse "." $ toList $ mods :< base
|
||||||
|
|
||||||
export Show Name where show = show . toPName
|
export Show Name where show = show . toPName
|
||||||
|
|
||||||
|
|
|
@ -89,7 +89,8 @@ terminalMatch what l r = terminalMatchN_ what [(l, r)]
|
||||||
||| tag without leading `'`
|
||| tag without leading `'`
|
||||||
export
|
export
|
||||||
bareTag : Grammar True TagVal
|
bareTag : Grammar True TagVal
|
||||||
bareTag = terminalMatchN "bare tag" [(`(Name t), `(show t)), (`(Str s), `(s))]
|
bareTag = terminalMatchN "bare tag"
|
||||||
|
[(`(Name t), `(toDotsP t)), (`(Str s), `(s))]
|
||||||
|
|
||||||
||| tag with leading quote
|
||| tag with leading quote
|
||||||
export
|
export
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
collection = "nightly-230505"
|
collection = "nightly-230522"
|
||||||
|
|
||||||
[custom.all.tap]
|
[custom.all.tap]
|
||||||
type = "git"
|
type = "git"
|
||||||
|
|
|
@ -1,78 +0,0 @@
|
||||||
open import Axiom.Extensionality.Propositional
|
|
||||||
|
|
||||||
module _ (ext : ∀ {a b} → Extensionality a b) where
|
|
||||||
|
|
||||||
open import Prelude hiding (zero; suc)
|
|
||||||
open import Data.W renaming (induction to induction′)
|
|
||||||
open import Data.Container
|
|
||||||
open import Data.Container.Relation.Unary.All ; open □
|
|
||||||
|
|
||||||
variable
|
|
||||||
𝓀 ℓ : Level
|
|
||||||
A B : Set 𝓀
|
|
||||||
P Q : A → Set ℓ
|
|
||||||
C : Container 𝓀 ℓ
|
|
||||||
|
|
||||||
|
|
||||||
data Tag : Set where `zero `suc : Tag
|
|
||||||
|
|
||||||
Body : Tag → Set
|
|
||||||
Body t = case t of λ {`zero → ⊥ ; `suc → ⊤}
|
|
||||||
|
|
||||||
Repr : Container lzero lzero
|
|
||||||
Repr = Tag ▷ Body
|
|
||||||
|
|
||||||
Nat : Set
|
|
||||||
Nat = W Repr
|
|
||||||
|
|
||||||
Nat′ : Set
|
|
||||||
Nat′ = ⟦ Repr ⟧ Nat
|
|
||||||
|
|
||||||
zero : Nat
|
|
||||||
zero = sup (`zero , λ ())
|
|
||||||
|
|
||||||
suc : Nat → Nat
|
|
||||||
suc n = sup (`suc , const n)
|
|
||||||
|
|
||||||
induction :
|
|
||||||
(P : W C → Set ℓ) →
|
|
||||||
(IH : (t : ⟦ C ⟧ (W C)) → □ C P t → P (sup t)) →
|
|
||||||
(w : W C) → P w
|
|
||||||
induction P IH = induction′ P (λ {t} → IH t)
|
|
||||||
|
|
||||||
|
|
||||||
elim : (P : Nat → Set ℓ) →
|
|
||||||
(Z : P zero) →
|
|
||||||
(S : ∀ n → P n → P (suc n)) →
|
|
||||||
(n : Nat) → P n
|
|
||||||
elim P Z S = induction _ λ (tag , body) →
|
|
||||||
body |>
|
|
||||||
(case tag
|
|
||||||
return (λ t → (n′ : Body t → Nat) →
|
|
||||||
□ Repr P (t , n′) →
|
|
||||||
P (sup (t , n′)))
|
|
||||||
of λ where
|
|
||||||
`zero → λ n′ _ → ≡.subst (λ n′ → P (sup (`zero , n′))) (ext λ ()) Z
|
|
||||||
`suc → λ n′ IH → S (n′ tt) (IH .proof tt))
|
|
||||||
|
|
||||||
pred : Nat → Nat
|
|
||||||
pred = induction _ λ n@(tag , body) _ →
|
|
||||||
body |>
|
|
||||||
(case tag
|
|
||||||
return (λ t → (Body t → Nat) → Nat)
|
|
||||||
of λ where
|
|
||||||
`zero _ → zero
|
|
||||||
`suc n → n tt)
|
|
||||||
|
|
||||||
Subterms : (A : Set 𝓀) (P : A → Set ℓ) → Set _
|
|
||||||
Subterms A P = Σ[ x ∈ A ] (P x → W (A ▷ P))
|
|
||||||
|
|
||||||
subterms : W (A ▷ P) → Subterms A P
|
|
||||||
subterms = induction _ λ t IH → t
|
|
||||||
|
|
||||||
natSub : Nat → List Nat
|
|
||||||
natSub n =
|
|
||||||
case subterms n of λ where
|
|
||||||
(`zero , body) → []
|
|
||||||
(`suc , body) → [ body tt ]
|
|
||||||
where open List
|
|
Loading…
Reference in New Issue