diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-27 20:32:03 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-27 20:32:03 +0000 |
| commit | adad5280af0d81a2f171df619e9c7169dcb43a02 (patch) | |
| tree | c537696feea2aec1688d398bf5fd93e76f72c702 /src/Cfe/Expression/Base.agda | |
| parent | c67134fc5cb9e338cb397df029e5528d469771d4 (diff) | |
Introduce non-terminating proof of derivation existence.
Diffstat (limited to 'src/Cfe/Expression/Base.agda')
| -rw-r--r-- | src/Cfe/Expression/Base.agda | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda index c3367c2..dd9e9b4 100644 --- a/src/Cfe/Expression/Base.agda +++ b/src/Cfe/Expression/Base.agda @@ -88,3 +88,12 @@ rotate (μ e) i j i≤j = μ (rotate e (suc i) (suc j) (s≤s i≤j)) _≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc (c ⊔ ℓ)) e₁ ≋ e₂ = ∀ γ → ⟦ e₁ ⟧ γ 𝕃.≈ ⟦ e₂ ⟧ γ + +rank : {n : ℕ} → Expression n → ℕ +rank ⊥ = 0 +rank ε = 0 +rank (Char _) = 0 +rank (e₁ ∨ e₂) = suc (rank e₁ ℕ.+ rank e₂) +rank (e₁ ∙ _) = suc (rank e₁) +rank (Var _) = 0 +rank (μ e) = suc (rank e) |