------------------------------------------------------------------------ -- The Agda standard library -- -- A universe for the types involved in the reflected syntax. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Reflection.AST.Universe where open import Data.List.Base using (List) open import Data.String.Base using (String) open import Data.Product.Base using (_×_) open import Reflection.AST.Argument using (Arg) open import Reflection.AST.Abstraction using (Abs) open import Reflection.AST.Term using (Term; Pattern; Sort; Clause) data Univ : Set where ⟨term⟩ : Univ ⟨pat⟩ : Univ ⟨sort⟩ : Univ ⟨clause⟩ : Univ ⟨list⟩ : Univ → Univ ⟨arg⟩ : Univ → Univ ⟨abs⟩ : Univ → Univ ⟨named⟩ : Univ → Univ pattern ⟨tel⟩ = ⟨list⟩ (⟨named⟩ (⟨arg⟩ ⟨term⟩)) ⟦_⟧ : Univ → Set ⟦ ⟨term⟩ ⟧ = Term ⟦ ⟨pat⟩ ⟧ = Pattern ⟦ ⟨sort⟩ ⟧ = Sort ⟦ ⟨clause⟩ ⟧ = Clause ⟦ ⟨list⟩ k ⟧ = List ⟦ k ⟧ ⟦ ⟨arg⟩ k ⟧ = Arg ⟦ k ⟧ ⟦ ⟨abs⟩ k ⟧ = Abs ⟦ k ⟧ ⟦ ⟨named⟩ k ⟧ = String × ⟦ k ⟧
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4