Frex.Free.Construction.Idris

Definitions

display : Printer pres () -> Proof pres lhs rhs -> Doc ()

Totality: total
Visibility: export

idris : Ord (Op (pres .signature)) => DecEq (Op (pres .signature)) => Finite (Op (pres .signature)) => Finite (pres .Axiom) => Printer pres () -> List String -> List (String, Lemma pres) -> String

Totality: total
Visibility: export