git.iko.soy/Idris-dev
on ca34dec help sign in
Idris-dev/test/reg075/expected
6 lines 270 B history raw
1data Foo : Bar m BMODEL -> Model ty -> FTy -> Type where
2 FElem : (name : String) -> Foo p (MElem name) FELEM
3 FLink : Foo p x FELEM ->
4 (c : Common) ->
5 (f : Bar g BELEM) ->
6 {auto prf : isValid f p = Yes prf'} -> Foo p (MLink c x g) FLINK