------------------------------------------------------------------------
-- The Agda standard library
--
-- Terms used in the reflection machinery
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.AST.Term where
open import Data.List.Base as List hiding (_++_)
open import Data.List.Properties using (∷-dec)
open import Data.Nat.Base using (ℕ; zero; suc)
import Data.Nat.Properties as ℕ using (_≟_)
open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁)
open import Data.Product.Properties using (,-injective)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.String.Base using (String)
open import Data.String.Properties as String hiding (_≟_)
open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no)
open import Relation.Binary.Definitions using (Decidable; DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
open import Reflection.AST.Abstraction using (Abs; abs; unAbs-dec)
open import Reflection.AST.Argument as Arg
open import Reflection.AST.Argument.Information using (visibility)
open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_)
import Reflection.AST.Literal as Literal using (Literal; _≟_)
import Reflection.AST.Meta as Meta using (Meta; _≟_)
open import Reflection.AST.Name as Name using (Name)
------------------------------------------------------------------------
-- Re-exporting the builtin type and constructors
open import Agda.Builtin.Reflection as Builtin public
using (Sort; Type; Term; Clause; Pattern)
open Term public
renaming (agda-sort to sort)
open Sort public
open Clause public
open Pattern public
------------------------------------------------------------------------
-- Handy synonyms
Clauses : Set
Clauses = List Clause
Telescope : Set
Telescope = List (String × Arg Type)
-- Pattern synonyms for more compact presentation
pattern vLam s t = lam visible (abs s t)
pattern hLam s t = lam hidden (abs s t)
pattern iLam s t = lam instance′ (abs s t)
pattern Π[_∶_]_ s a ty = pi a (abs s ty)
pattern vΠ[_∶_]_ s a ty = Π[ s ∶ (vArg a) ] ty
pattern hΠ[_∶_]_ s a ty = Π[ s ∶ (hArg a) ] ty
pattern iΠ[_∶_]_ s a ty = Π[ s ∶ (iArg a) ] ty
------------------------------------------------------------------------
-- Utility functions
getName : Term → Maybe Name
getName (con c args) = just c
getName (def f args) = just f
getName _ = nothing
-- "n ⋯⟨∷⟩ xs" prepends "n" visible unknown arguments to the list of
-- arguments. Useful when constructing the list of arguments for a
-- function with initial inferrable arguments.
infixr 5 _⋯⟨∷⟩_
_⋯⟨∷⟩_ : ℕ → Args Term → Args Term
zero ⋯⟨∷⟩ xs = xs
suc i ⋯⟨∷⟩ xs = unknown ⟨∷⟩ (i ⋯⟨∷⟩ xs)
{-# INLINE _⋯⟨∷⟩_ #-}
-- "n ⋯⟅∷⟆ xs" prepends "n" hidden unknown arguments to the list of
-- arguments. Useful when constructing the list of arguments for a
-- function with initial implicit arguments.
infixr 5 _⋯⟅∷⟆_
_⋯⟅∷⟆_ : ℕ → Args Term → Args Term
zero ⋯⟅∷⟆ xs = xs
suc i ⋯⟅∷⟆ xs = unknown ⟅∷⟆ (i ⋯⟅∷⟆ xs)
{-# INLINE _⋯⟅∷⟆_ #-}
-- Strips off any pi bindings returning the list of variables removed
-- and the eventual body of the expression, e.g.
--
-- stripPis `∀ x {y} → f x y` = (["x", "y"], f x y)
stripPis : Term → List (String × Arg Type) × Term
stripPis (Π[ s ∶ t ] x) = map₁ ((s , t) ∷_) (stripPis x)
stripPis x = [] , x
prependLams : List (String × Visibility) → Term → Term
prependLams xs t = foldr (λ {(s , v) t → lam v (abs s t)}) t (reverse xs)
prependHLams : List String → Term → Term
prependHLams vs = prependLams (List.map (_, hidden) vs)
prependVLams : List String → Term → Term
prependVLams vs = prependLams (List.map (_, visible) vs)
------------------------------------------------------------------------
-- Decidable equality
clause-injective₁ : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → tel ≡ tel′
clause-injective₁ refl = refl
clause-injective₂ : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → ps ≡ ps′
clause-injective₂ refl = refl
clause-injective₃ : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → b ≡ b′
clause-injective₃ refl = refl
clause-injective : ∀ {tel tel′ ps ps′ b b′} → clause tel ps b ≡ clause tel′ ps′ b′ → tel ≡ tel′ × ps ≡ ps′ × b ≡ b′
clause-injective = < clause-injective₁ , < clause-injective₂ , clause-injective₃ > >
absurd-clause-injective₁ : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → tel ≡ tel′
absurd-clause-injective₁ refl = refl
absurd-clause-injective₂ : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → ps ≡ ps′
absurd-clause-injective₂ refl = refl
absurd-clause-injective : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → tel ≡ tel′ × ps ≡ ps′
absurd-clause-injective = < absurd-clause-injective₁ , absurd-clause-injective₂ >
infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
_≟-Clause_ _≟-Clauses_ _≟_
_≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_
_≟-AbsTerm_ : DecidableEquality (Abs Term)
_≟-AbsType_ : DecidableEquality (Abs Type)
_≟-ArgTerm_ : DecidableEquality (Arg Term)
_≟-ArgType_ : DecidableEquality (Arg Type)
_≟-Args_ : DecidableEquality (Args Term)
_≟-Clause_ : DecidableEquality Clause
_≟-Clauses_ : DecidableEquality Clauses
_≟_ : DecidableEquality Term
_≟-Sort_ : DecidableEquality Sort
_≟-Patterns_ : DecidableEquality (Args Pattern)
_≟-Pattern_ : DecidableEquality Pattern
-- Decidable equality 'transformers'
-- We need to inline these because the terms are not sized so
-- termination would not obvious if we were to use higher-order
-- functions such as Data.List.Properties' ≡-dec
abs s a ≟-AbsTerm abs s′ a′ = unAbs-dec (a ≟ a′)
abs s a ≟-AbsType abs s′ a′ = unAbs-dec (a ≟ a′)
arg i a ≟-ArgTerm arg i′ a′ = unArg-dec (a ≟ a′)
arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′)
[] ≟-Args [] = yes refl
(x ∷ xs) ≟-Args (y ∷ ys) = ∷-dec (x ≟-ArgTerm y) (xs ≟-Args ys)
[] ≟-Args (_ ∷ _) = no λ()
(_ ∷ _) ≟-Args [] = no λ()
[] ≟-Clauses [] = yes refl
(x ∷ xs) ≟-Clauses (y ∷ ys) = ∷-dec (x ≟-Clause y) (xs ≟-Clauses ys)
[] ≟-Clauses (_ ∷ _) = no λ()
(_ ∷ _) ≟-Clauses [] = no λ()
_≟-Telescope_ : DecidableEquality Telescope
[] ≟-Telescope [] = yes refl
((x , t) ∷ tel) ≟-Telescope ((x′ , t′) ∷ tel′) = ∷-dec
(map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′)))
(tel ≟-Telescope tel′)
[] ≟-Telescope (_ ∷ _) = no λ ()
(_ ∷ _) ≟-Telescope [] = no λ ()
clause tel ps b ≟-Clause clause tel′ ps′ b′ =
map′ (λ (tel≡tel′ , ps≡ps′ , b≡b′) → cong₂ (uncurry clause) (cong₂ _,_ tel≡tel′ ps≡ps′) b≡b′)
clause-injective
(tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′ ×-dec b ≟ b′)
absurd-clause tel ps ≟-Clause absurd-clause tel′ ps′ =
map′ (uncurry (cong₂ absurd-clause))
absurd-clause-injective
(tel ≟-Telescope tel′ ×-dec ps ≟-Patterns ps′)
clause _ _ _ ≟-Clause absurd-clause _ _ = no λ()
absurd-clause _ _ ≟-Clause clause _ _ _ = no λ()
var-injective₁ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → x ≡ x′
var-injective₁ refl = refl
var-injective₂ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → args ≡ args′
var-injective₂ refl = refl
var-injective : ∀ {x x′ args args′} → var x args ≡ var x′ args′ → x ≡ x′ × args ≡ args′
var-injective = < var-injective₁ , var-injective₂ >
con-injective₁ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → c ≡ c′
con-injective₁ refl = refl
con-injective₂ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → args ≡ args′
con-injective₂ refl = refl
con-injective : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′ × args ≡ args′
con-injective = < con-injective₁ , con-injective₂ >
def-injective₁ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → f ≡ f′
def-injective₁ refl = refl
def-injective₂ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → args ≡ args′
def-injective₂ refl = refl
def-injective : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → f ≡ f′ × args ≡ args′
def-injective = < def-injective₁ , def-injective₂ >
meta-injective₁ : ∀ {x x′ args args′} → meta x args ≡ meta x′ args′ → x ≡ x′
meta-injective₁ refl = refl
meta-injective₂ : ∀ {x x′ args args′} → meta x args ≡ meta x′ args′ → args ≡ args′
meta-injective₂ refl = refl
meta-injective : ∀ {x x′ args args′} → meta x args ≡ meta x′ args′ → x ≡ x′ × args ≡ args′
meta-injective = < meta-injective₁ , meta-injective₂ >
lam-injective₁ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → v ≡ v′
lam-injective₁ refl = refl
lam-injective₂ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → t ≡ t′
lam-injective₂ refl = refl
lam-injective : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → v ≡ v′ × t ≡ t′
lam-injective = < lam-injective₁ , lam-injective₂ >
pat-lam-injective₁ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → cs ≡ cs′
pat-lam-injective₁ refl = refl
pat-lam-injective₂ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → args ≡ args′
pat-lam-injective₂ refl = refl
pat-lam-injective : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → cs ≡ cs′ × args ≡ args′
pat-lam-injective = < pat-lam-injective₁ , pat-lam-injective₂ >
pi-injective₁ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₁ ≡ t₁′
pi-injective₁ refl = refl
pi-injective₂ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₂ ≡ t₂′
pi-injective₂ refl = refl
pi-injective : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₁ ≡ t₁′ × t₂ ≡ t₂′
pi-injective = < pi-injective₁ , pi-injective₂ >
sort-injective : ∀ {x y} → sort x ≡ sort y → x ≡ y
sort-injective refl = refl
lit-injective : ∀ {x y} → lit x ≡ lit y → x ≡ y
lit-injective refl = refl
set-injective : ∀ {x y} → set x ≡ set y → x ≡ y
set-injective refl = refl
slit-injective : ∀ {x y} → Sort.lit x ≡ lit y → x ≡ y
slit-injective refl = refl
prop-injective : ∀ {x y} → prop x ≡ prop y → x ≡ y
prop-injective refl = refl
propLit-injective : ∀ {x y} → propLit x ≡ propLit y → x ≡ y
propLit-injective refl = refl
inf-injective : ∀ {x y} → inf x ≡ inf y → x ≡ y
inf-injective refl = refl
var x args ≟ var x′ args′ =
map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×-dec args ≟-Args args′)
con c args ≟ con c′ args′ =
map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×-dec args ≟-Args args′)
def f args ≟ def f′ args′ =
map′ (uncurry (cong₂ def)) def-injective (f Name.≟ f′ ×-dec args ≟-Args args′)
meta x args ≟ meta x′ args′ =
map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≟ x′ ×-dec args ≟-Args args′)
lam v t ≟ lam v′ t′ =
map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≟ v′ ×-dec t ≟-AbsTerm t′)
pat-lam cs args ≟ pat-lam cs′ args′ =
map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≟-Clauses cs′ ×-dec args ≟-Args args′)
pi t₁ t₂ ≟ pi t₁′ t₂′ =
map′ (uncurry (cong₂ pi)) pi-injective (t₁ ≟-ArgType t₁′ ×-dec t₂ ≟-AbsType t₂′)
sort s ≟ sort s′ = map′ (cong sort) sort-injective (s ≟-Sort s′)
lit l ≟ lit l′ = map′ (cong lit) lit-injective (l Literal.≟ l′)
unknown ≟ unknown = yes refl
var x args ≟ con c args′ = no λ()
var x args ≟ def f args′ = no λ()
var x args ≟ lam v t = no λ()
var x args ≟ pi t₁ t₂ = no λ()
var x args ≟ sort _ = no λ()
var x args ≟ lit _ = no λ()
var x args ≟ meta _ _ = no λ()
var x args ≟ unknown = no λ()
con c args ≟ var x args′ = no λ()
con c args ≟ def f args′ = no λ()
con c args ≟ lam v t = no λ()
con c args ≟ pi t₁ t₂ = no λ()
con c args ≟ sort _ = no λ()
con c args ≟ lit _ = no λ()
con c args ≟ meta _ _ = no λ()
con c args ≟ unknown = no λ()
def f args ≟ var x args′ = no λ()
def f args ≟ con c args′ = no λ()
def f args ≟ lam v t = no λ()
def f args ≟ pi t₁ t₂ = no λ()
def f args ≟ sort _ = no λ()
def f args ≟ lit _ = no λ()
def f args ≟ meta _ _ = no λ()
def f args ≟ unknown = no λ()
lam v t ≟ var x args = no λ()
lam v t ≟ con c args = no λ()
lam v t ≟ def f args = no λ()
lam v t ≟ pi t₁ t₂ = no λ()
lam v t ≟ sort _ = no λ()
lam v t ≟ lit _ = no λ()
lam v t ≟ meta _ _ = no λ()
lam v t ≟ unknown = no λ()
pi t₁ t₂ ≟ var x args = no λ()
pi t₁ t₂ ≟ con c args = no λ()
pi t₁ t₂ ≟ def f args = no λ()
pi t₁ t₂ ≟ lam v t = no λ()
pi t₁ t₂ ≟ sort _ = no λ()
pi t₁ t₂ ≟ lit _ = no λ()
pi t₁ t₂ ≟ meta _ _ = no λ()
pi t₁ t₂ ≟ unknown = no λ()
sort _ ≟ var x args = no λ()
sort _ ≟ con c args = no λ()
sort _ ≟ def f args = no λ()
sort _ ≟ lam v t = no λ()
sort _ ≟ pi t₁ t₂ = no λ()
sort _ ≟ lit _ = no λ()
sort _ ≟ meta _ _ = no λ()
sort _ ≟ unknown = no λ()
lit _ ≟ var x args = no λ()
lit _ ≟ con c args = no λ()
lit _ ≟ def f args = no λ()
lit _ ≟ lam v t = no λ()
lit _ ≟ pi t₁ t₂ = no λ()
lit _ ≟ sort _ = no λ()
lit _ ≟ meta _ _ = no λ()
lit _ ≟ unknown = no λ()
meta _ _ ≟ var x args = no λ()
meta _ _ ≟ con c args = no λ()
meta _ _ ≟ def f args = no λ()
meta _ _ ≟ lam v t = no λ()
meta _ _ ≟ pi t₁ t₂ = no λ()
meta _ _ ≟ sort _ = no λ()
meta _ _ ≟ lit _ = no λ()
meta _ _ ≟ unknown = no λ()
unknown ≟ var x args = no λ()
unknown ≟ con c args = no λ()
unknown ≟ def f args = no λ()
unknown ≟ lam v t = no λ()
unknown ≟ pi t₁ t₂ = no λ()
unknown ≟ sort _ = no λ()
unknown ≟ lit _ = no λ()
unknown ≟ meta _ _ = no λ()
pat-lam _ _ ≟ var x args = no λ()
pat-lam _ _ ≟ con c args = no λ()
pat-lam _ _ ≟ def f args = no λ()
pat-lam _ _ ≟ lam v t = no λ()
pat-lam _ _ ≟ pi t₁ t₂ = no λ()
pat-lam _ _ ≟ sort _ = no λ()
pat-lam _ _ ≟ lit _ = no λ()
pat-lam _ _ ≟ meta _ _ = no λ()
pat-lam _ _ ≟ unknown = no λ()
var x args ≟ pat-lam _ _ = no λ()
con c args ≟ pat-lam _ _ = no λ()
def f args ≟ pat-lam _ _ = no λ()
lam v t ≟ pat-lam _ _ = no λ()
pi t₁ t₂ ≟ pat-lam _ _ = no λ()
sort _ ≟ pat-lam _ _ = no λ()
lit _ ≟ pat-lam _ _ = no λ()
meta _ _ ≟ pat-lam _ _ = no λ()
unknown ≟ pat-lam _ _ = no λ()
set t ≟-Sort set t′ = map′ (cong set) set-injective (t ≟ t′)
lit n ≟-Sort lit n′ = map′ (cong lit) slit-injective (n ℕ.≟ n′)
prop t ≟-Sort prop t′ = map′ (cong prop) prop-injective (t ≟ t′)
propLit n ≟-Sort propLit n′ = map′ (cong propLit) propLit-injective (n ℕ.≟ n′)
inf n ≟-Sort inf n′ = map′ (cong inf) inf-injective (n ℕ.≟ n′)
unknown ≟-Sort unknown = yes refl
set _ ≟-Sort lit _ = no λ()
set _ ≟-Sort prop _ = no λ()
set _ ≟-Sort propLit _ = no λ()
set _ ≟-Sort inf _ = no λ()
set _ ≟-Sort unknown = no λ()
lit _ ≟-Sort set _ = no λ()
lit _ ≟-Sort prop _ = no λ()
lit _ ≟-Sort propLit _ = no λ()
lit _ ≟-Sort inf _ = no λ()
lit _ ≟-Sort unknown = no λ()
prop _ ≟-Sort set _ = no λ()
prop _ ≟-Sort lit _ = no λ()
prop _ ≟-Sort propLit _ = no λ()
prop _ ≟-Sort inf _ = no λ()
prop _ ≟-Sort unknown = no λ()
propLit _ ≟-Sort set _ = no λ()
propLit _ ≟-Sort lit _ = no λ()
propLit _ ≟-Sort prop _ = no λ()
propLit _ ≟-Sort inf _ = no λ()
propLit _ ≟-Sort unknown = no λ()
inf _ ≟-Sort set _ = no λ()
inf _ ≟-Sort lit _ = no λ()
inf _ ≟-Sort prop _ = no λ()
inf _ ≟-Sort propLit _ = no λ()
inf _ ≟-Sort unknown = no λ()
unknown ≟-Sort set _ = no λ()
unknown ≟-Sort lit _ = no λ()
unknown ≟-Sort prop _ = no λ()
unknown ≟-Sort propLit _ = no λ()
unknown ≟-Sort inf _ = no λ()
pat-con-injective₁ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′
pat-con-injective₁ refl = refl
pat-con-injective₂ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → args ≡ args′
pat-con-injective₂ refl = refl
pat-con-injective : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′ × args ≡ args′
pat-con-injective = < pat-con-injective₁ , pat-con-injective₂ >
pat-var-injective : ∀ {x y} → var x ≡ var y → x ≡ y
pat-var-injective refl = refl
pat-lit-injective : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y
pat-lit-injective refl = refl
proj-injective : ∀ {x y} → proj x ≡ proj y → x ≡ y
proj-injective refl = refl
dot-injective : ∀ {x y} → dot x ≡ dot y → x ≡ y
dot-injective refl = refl
absurd-injective : ∀ {x y} → absurd x ≡ absurd y → x ≡ y
absurd-injective refl = refl
con c ps ≟-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≟ c′ ×-dec ps ≟-Patterns ps′)
var x ≟-Pattern var x′ = map′ (cong var) pat-var-injective (x ℕ.≟ x′)
lit l ≟-Pattern lit l′ = map′ (cong lit) pat-lit-injective (l Literal.≟ l′)
proj a ≟-Pattern proj a′ = map′ (cong proj) proj-injective (a Name.≟ a′)
dot t ≟-Pattern dot t′ = map′ (cong dot) dot-injective (t ≟ t′)
absurd x ≟-Pattern absurd x′ = map′ (cong absurd) absurd-injective (x ℕ.≟ x′)
con x x₁ ≟-Pattern dot x₂ = no (λ ())
con x x₁ ≟-Pattern var x₂ = no (λ ())
con x x₁ ≟-Pattern lit x₂ = no (λ ())
con x x₁ ≟-Pattern proj x₂ = no (λ ())
con x x₁ ≟-Pattern absurd x₂ = no (λ ())
dot x ≟-Pattern con x₁ x₂ = no (λ ())
dot x ≟-Pattern var x₁ = no (λ ())
dot x ≟-Pattern lit x₁ = no (λ ())
dot x ≟-Pattern proj x₁ = no (λ ())
dot x ≟-Pattern absurd x₁ = no (λ ())
var s ≟-Pattern con x x₁ = no (λ ())
var s ≟-Pattern dot x = no (λ ())
var s ≟-Pattern lit x = no (λ ())
var s ≟-Pattern proj x = no (λ ())
var s ≟-Pattern absurd x = no (λ ())
lit x ≟-Pattern con x₁ x₂ = no (λ ())
lit x ≟-Pattern dot x₁ = no (λ ())
lit x ≟-Pattern var _ = no (λ ())
lit x ≟-Pattern proj x₁ = no (λ ())
lit x ≟-Pattern absurd x₁ = no (λ ())
proj x ≟-Pattern con x₁ x₂ = no (λ ())
proj x ≟-Pattern dot x₁ = no (λ ())
proj x ≟-Pattern var _ = no (λ ())
proj x ≟-Pattern lit x₁ = no (λ ())
proj x ≟-Pattern absurd x₁ = no (λ ())
absurd x ≟-Pattern con x₁ x₂ = no (λ ())
absurd x ≟-Pattern dot x₁ = no (λ ())
absurd x ≟-Pattern var _ = no (λ ())
absurd x ≟-Pattern lit x₁ = no (λ ())
absurd x ≟-Pattern proj x₁ = no (λ ())
[] ≟-Patterns [] = yes refl
(arg i p ∷ xs) ≟-Patterns (arg j q ∷ ys) = ∷-dec (unArg-dec (p ≟-Pattern q)) (xs ≟-Patterns ys)
[] ≟-Patterns (_ ∷ _) = no λ()
(_ ∷ _) ≟-Patterns [] = no λ()
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