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 Unused = "_"
|
||||
|
||||
export Show BaseName where show = baseStr
|
||||
export Show BaseName where show = show . baseStr
|
||||
export FromString BaseName where fromString = UN
|
||||
|
||||
|
||||
|
@ -82,7 +82,8 @@ fromPBaseName = MakeName [<] . UN
|
|||
|
||||
export
|
||||
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
|
||||
|
||||
|
|
|
@ -89,7 +89,8 @@ terminalMatch what l r = terminalMatchN_ what [(l, r)]
|
|||
||| tag without leading `'`
|
||||
export
|
||||
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
|
||||
export
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
collection = "nightly-230505"
|
||||
collection = "nightly-230522"
|
||||
|
||||
[custom.all.tap]
|
||||
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