私の等価性のためにリライトを使用していますか？

Question

私は平等の次の定義を持っている：私はrewrite構文を使用したいときはいつでも

data Equal : x -> y -> Type where 
    Reflexive : Equal a a 

、私はタイプ(a = b)の何かを必要とするので、私は作成しました：

makeEquitable : Equal x y -> x = y 
makeEquitable Reflexive = Refl 

今私はmakeEquitable (_ : Equal a b)れを行うことができます私はrewriteものに使用することができます。私はこれを簡素化したいと私はreplace : (x = y) -> P x -> P yを理解してreplaceに見えた。このPものは、私が想定している内蔵のIdrisプロパティです。私自身の定義のために、どうすればこのような機能を作りますか？rewriteは、魔法のようにEqual a bのために働くように特別な "焼き付け"が可能でしょうか？あなたはREPLで:set showimplicitsを設定した場合

Answer 1

は、あなたが:t replaceのための暗黙の引数を参照してくださいについてP特別なものは何もありません

replace : {a : Type} -> {x : a} -> {y : a} -> {P : a -> Type} -> 
      ((=) {A = a} {B = a} x y) -> P x -> P y 

、それだけで暗黙の引数である：タイプの値の上に保持している述語Pa。

replaceEqual : {P : a -> Type} -> Equal x y -> P x -> P y 
replaceEqual Reflexive prf = prf 

しかし、あなたは簡単に私の知る限りrewrite独自のものを作ることができない：あなたの関数がどのように見えることができるようにこれらの暗黙の引数のほとんどの種類は、推測することができます。ただし、構文ルールを使用してアプローチを肯定することができます。

syntax eqrewrite [a] "in" [b] = rewrite makeEquitable a in b; 

plus_commutes_Z' : Equal m (plus m 0) 
plus_commutes_Z' {m = Z} = Reflexive 
plus_commutes_Z' {m = (S k)} = 
    let rec = plus_commutes_Z' {m=k} 
    in eqrewrite rec in Reflexive